---

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

.....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
BY
{ ((Assert ∀k:ℕ. (q * (1/2) ↑ k ∈ {q:ℚ| 0 < q} ) BY
          (Auto
           THEN DVar `q'
           THEN MemTypeCD
           THEN Auto
           THEN BLemma `qmul-positive`
           THEN Auto
           THEN OrLeft
           THEN Auto
           THEN Try ((BLemma `qexp-positive` THEN Auto))
           THEN QMul ⌈2⌉ 0⋅
           THEN Auto))
   THEN PromoteHyp (-1) 3
   ) }

1
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 ∈ ℤ)
⊢ E(n;λs.imax-list(map(λi.(F i (q * (1/2) ↑ i + 1) <n, s>);upto(n)))) < q

---

Latex:


.....falsecase..... 
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.  \mneg{}(n  =  0)
\mvdash{}  E(n;\mlambda{}s.imax-list(map(\mlambda{}i.(F  i  (q  *  (1/2)  \muparrow{}  i  +  1)  <n,  s>);upto(n))))  <  q


By

((Assert  \mforall{}k:\mBbbN{}.  (q  *  (1/2)  \muparrow{}  k  \mmember{}  \{q:\mBbbQ{}|  0  <  q\}  )  BY
                (Auto
                  THEN  DVar  `q'
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  BLemma  `qmul-positive`
                  THEN  Auto
                  THEN  OrLeft
                  THEN  Auto
                  THEN  Try  ((BLemma  `qexp-positive`  THEN  Auto))
                  THEN  QMul  \mkleeneopen{}2\mkleeneclose{}  0\mcdot{}
                  THEN  Auto))
  THEN  PromoteHyp  (-1)  3
  )

---

Home Index