---

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index