---

Step * 1 of Lemma nullset-union


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)
BY
{ (Reduce 0 THEN (InstConcl [⌈countable-p-union(i.F i (q * (1/2) ↑ i + 1))⌉]⋅ THENA Auto)) }

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)
7. i : ℕ@i
⊢ q * (1/2) ↑ i + 1 ∈ {q:ℚ| 0 < q} 

2
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)
⊢ (∀s:ℕ ─→ Outcome. ((∃i:ℕ. (S[i] s)) ⇒ s ∈ countable-p-union(i.F i (q * (1/2) ↑ i + 1))))
∧ measure(countable-p-union(i.F i (q * (1/2) ↑ i + 1))) ≤ q

---

Latex:



1.  p  :  FinProbSpace@i
2.  [S]  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  {}\mrightarrow{}  Outcome)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .    \mexists{}C:p-open(p).  ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  ((S[i]  s)  {}\mRightarrow{}  s  \mmember{}  C))  \mwedge{}  measure(C)  \mleq{}  q)@\000Ci
4.  q  :  \{q:\mBbbQ{}|  0  <  q\}  @i
5.  F  :  \mBbbN{}  {}\mrightarrow{}  \{q:\mBbbQ{}|  0  <  q\}    {}\mrightarrow{}  p-open(p)
6.  \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)
\mvdash{}  \mexists{}C:p-open(p).  ((\mforall{}s:\mBbbN{}  {}\mrightarrow{}  Outcome.  (((\mlambda{}s.\mexists{}i:\mBbbN{}.  (S[i]  s))  s)  {}\mRightarrow{}  s  \mmember{}  C))  \mwedge{}  measure(C)  \mleq{}  q)


By

(Reduce  0  THEN  (InstConcl  [\mkleeneopen{}countable-p-union(i.F  i  (q  *  (1/2)  \muparrow{}  i  +  1))\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index