---

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

.....assertion..... 
1. p : FinProbSpace@i
2. q : {q:ℚ| 0 < q} @i
3. ∀k:ℕ. (q * (1/2) ↑ k ∈ {q:ℚ| 0 < q} )
4. F : ℕ ─→ {q:ℚ| 0 < q}  ─→ p-open(p)@i
5. ∀i:ℕ. ∀q:{q:ℚ| 0 < q} .  measure(F i q) ≤ q@i
6. n : ℕ@i
7. ¬(n = 0 ∈ ℤ)
8. E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) ≤ Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n,\000C s>))
⊢ Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) < q
BY
{ Assert ⌈Σ0 ≤ i < n. E(n;λs.(F i (q * (1/2) ↑ i + 1) <n, s>)) ≤ Σ0 ≤ i < n. q * (1/2) ↑ i + 1⌉⋅ }

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

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

---

Latex:


.....assertion..... 
1.  p  :  FinProbSpace@i
2.  q  :  \{q:\mBbbQ{}|  0  <  q\}  @i
3.  \mforall{}k:\mBbbN{}.  (q  *  (1/2)  \muparrow{}  k  \mmember{}  \{q:\mBbbQ{}|  0  <  q\}  )
4.  F  :  \mBbbN{}  {}\mrightarrow{}  \{q:\mBbbQ{}|  0  <  q\}    {}\mrightarrow{}  p-open(p)@i
5.  \mforall{}i:\mBbbN{}.  \mforall{}q:\{q:\mBbbQ{}|  0  <  q\}  .    measure(F  i  q)  \mleq{}  q@i
6.  n  :  \mBbbN{}@i
7.  \mneg{}(n  =  0)
8.  E(n;\mlambda{}s.imax-list(map(\mlambda{}i.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>);upto(n))))  \mleq{}  \mSigma{}0  \mleq{}  i  <  n.  E(n;\mlambda{}s.(F  i  (q  \000C*  (1/2)  \muparrow{}  i  +  1)  <n,  s>))
\mvdash{}  \mSigma{}0  \mleq{}  i  <  n.  E(n;\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>))  <  q


By

Assert  \mkleeneopen{}\mSigma{}0  \mleq{}  i  <  n.  E(n;\mlambda{}s.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>))  \mleq{}  \mSigma{}0  \mleq{}  i  <  n.  q  *  (1/2)  \muparrow{}  i  +  1\mkleeneclose{}\mcdot{}

---

Home Index