---

Step * of Lemma nullset-union

∀p:FinProbSpace. ∀[S:ℕ ─→ (ℕ ─→ Outcome) ─→ ℙ]. ((∀i:ℕ. nullset(p;S[i])) ⇒ nullset(p;λs.∃i:ℕ. (S[i] s)))
BY
{ (Auto
   THEN (All (Unfold `nullset`))
   THEN Auto
   THEN (Assert ∃F:ℕ ─→ {q:ℚ| 0 < q}  ─→ p-open(p)
                 ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  ((∀s:ℕ ─→ Outcome. ((S[i] s) ⇒ s ∈ F i q)) ∧ measure(F i q) ≤ q) BY
               ((RenameVar `f' (-2))
                THEN InstConcl [⌈λi,q. (fst((f i q)))⌉]⋅
                THEN Auto
                THEN Reduce 0
                THEN (GenConcl ⌈(f i q1)
                                = Z
                                ∈ (∃C:p-open(p). ((∀s:ℕ ─→ Outcome. ((S[i] s) ⇒ s ∈ C)) ∧ measure(C) ≤ q1))⌉⋅
                      THENA Auto
                      )
                THEN D -2
                THEN Reduce 0
                THEN Auto))
   THEN ExRepD) }

1
1. p : FinProbSpace@i
2. [S] : ℕ ─→ (ℕ ─→ Outcome) ─→ ℙ
3. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  ∃C:p-open(p). ((∀s:ℕ ─→ Outcome. ((S[i] s) ⇒ s ∈ C)) ∧ measure(C) ≤ q)@i
4. q : {q:ℚ| 0 < q} @i
5. F : ℕ ─→ {q:ℚ| 0 < q}  ─→ p-open(p)
6. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  ((∀s:ℕ ─→ Outcome. ((S[i] s) ⇒ s ∈ F i q)) ∧ measure(F i q) ≤ q)
⊢ ∃C:p-open(p). ((∀s:ℕ ─→ Outcome. (((λs.∃i:ℕ. (S[i] s)) s) ⇒ s ∈ C)) ∧ measure(C) ≤ q)

---

Latex:


\mforall{}p:FinProbSpace
    \mforall{}[S:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}i:\mBbbN{}.  nullset(p;S[i]))  {}\mRightarrow{}  nullset(p;\mlambda{}s.\mexists{}i:\mBbbN{}.  (S[i]  s)))


By

(Auto
  THEN  (All  (Unfold  `nullset`))
  THEN  Auto
  THEN  (Assert  \mexists{}F:\mBbbN{}  {}\mrightarrow{}  \{q:\mBbbQ{}|  0  <  q\}    {}\mrightarrow{}  p-open(p)
                              \mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .
                                  ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  ((S[i]  s)  {}\mRightarrow{}  s  \mmember{}  F  i  q))  \mwedge{}  measure(F  i  q)  \mleq{}  q)  BY
                          ((RenameVar  `f'  (-2))
                            THEN  InstConcl  [\mkleeneopen{}\mlambda{}i,q.  (fst((f  i  q)))\mkleeneclose{}]\mcdot{}
                            THEN  Auto
                            THEN  Reduce  0
                            THEN  (GenConcl  \mkleeneopen{}(f  i  q1)  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  ExRepD)

---

Home Index