---

Step * 1 2 2 1 of Lemma nullset-union


∀p:FinProbSpace. ∀q:{q:ℚ| 0 < q} . ∀F:ℕ ⟶ {q:ℚ| 0 < q}  ⟶ p-open(p).
  ((∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q) ⇒ measure(countable-p-union(i.F i (q * (1/2) ↑ i + 1))) ≤ q)
BY
{ xxx(Auto THEN D 0 THEN Auto THEN Unfold `countable-p-union` 0 THEN Reduce 0 THEN (SplitOnConclITE THENA Auto))xxx }

1
.....truecase..... 
1. p : FinProbSpace
2. q : {q:ℚ| 0 < q} 
3. F : ℕ ⟶ {q:ℚ| 0 < q}  ⟶ p-open(p)
4. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q
5. n : ℕ
6. n = 0 ∈ ℤ
⊢ E(n;λs.0) < q

2
.....falsecase..... 
1. p : FinProbSpace
2. q : {q:ℚ| 0 < q} 
3. F : ℕ ⟶ {q:ℚ| 0 < q}  ⟶ p-open(p)
4. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q
5. n : ℕ
6. ¬(n = 0 ∈ ℤ)
⊢ E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) < q

---

Latex:

---

Latex:

\mforall{}p:FinProbSpace.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .  \mforall{}F:\mBbbN{}  {}\mrightarrow{}  \{q:\mBbbQ{}|  0  <  q\}    {}\mrightarrow{}  p-open(p).
    ((\mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .    measure(F  i  q)  \mleq{}  q)
    {}\mRightarrow{}  measure(countable-p-union(i.F  i  (q  *  (1/2)  \muparrow{}  i  +  1)))  \mleq{}  q)


By

---

Latex:
xxx(Auto
        THEN  D  0
        THEN  Auto
        THEN  Unfold  `countable-p-union`  0
        THEN  Reduce  0
        THEN  (SplitOnConclITE  THENA  Auto))xxx

---

Home Index