---

Step * of Lemma nullset-union

∀p:FinProbSpace. ∀[S:ℕ ⟶ (ℕ ⟶ Outcome) ⟶ ℙ]. ((∀i:ℕ. nullset(p;S[i])) ⇒ nullset(p;λs.∃i:ℕ. (S[i] s)))
BY
{ xxx(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)xxx }

1
1. p : FinProbSpace
2. [S] : ℕ ⟶ (ℕ ⟶ Outcome) ⟶ ℙ
3. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  ∃C:p-open(p). ((∀s:ℕ ⟶ Outcome. ((S[i] s) ⇒ s ∈ C)) ∧ measure(C) ≤ q)
4. q : {q:ℚ| 0 < q} 
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:

---

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

---

Latex:
xxx(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)xxx

---

Home Index