---

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
{ (Auto THEN D 0 THEN Auto THEN Unfold `countable-p-union` 0 THEN Reduce 0 THEN (SplitOnConclITE THENA Auto)) }

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

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

---

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

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

---

Home Index