---

Step * 1 2 2 1 1 of Lemma nullset-union

.....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
BY
{ (Subst' E(n;λs.0) = 0 ∈ ℚ 0 THEN Auto) }

1
.....equality..... 
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) = 0 ∈ ℚ

---

Latex:


.....truecase..... 
1.  p  :  FinProbSpace@i
2.  q  :  \{q:\mBbbQ{}|  0  <  q\}  @i
3.  F  :  \mBbbN{}  {}\mrightarrow{}  \{q:\mBbbQ{}|  0  <  q\}    {}\mrightarrow{}  p-open(p)@i
4.  \mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .    measure(F  i  q)  \mleq{}  q@i
5.  n  :  \mBbbN{}@i
6.  n  =  0
\mvdash{}  E(n;\mlambda{}s.0)  <  q


By

(Subst'  E(n;\mlambda{}s.0)  =  0  0  THEN  Auto)

---

Home Index