---

Step * 1 of Lemma cantor-to-interval-req

.....assertion..... 
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. f : ℕ ⟶ 𝔹
5. ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))])
6. a ≤ b
⊢ lim n→∞.fst(cantor-interval(a;b;f;n)) = x
BY
{ TACTIC:(InstLemma `common-limit-squeeze-ext`
             [⌜λ2n.fst(cantor-interval(a;b;f;n))⌝
             ; ⌜λ2n.x⌝;⌜λ2n.(2^n * b - a)/3^n⌝]⋅
          THEN Auto
          THEN Try ((BLemma `cantor-interval-rless` THEN Auto))
          THEN Try ((BLemma `cantor-interval-inclusion`⋅ THEN Auto))
          THEN Try ((D 0 THEN RWO "cantor-interval-length" 0 THEN Auto))) }

1
.....antecedent..... 
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. f : ℕ ⟶ 𝔹
5. ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))])
6. a ≤ b
⊢ lim n→∞.(2^n * b - a)/3^n = r0

2
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. f : ℕ ⟶ 𝔹
5. ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))])
6. a ≤ b
7. n : ℕ
⊢ r0≤x - fst(cantor-interval(a;b;f;n))≤(2^n * b - a)/3^n

3
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. f : ℕ ⟶ 𝔹
5. ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))])
6. a ≤ b
7. ∃y:ℝ. (lim n→∞.fst(cantor-interval(a;b;f;n)) = y ∧ lim n→∞.x = y)
⊢ lim n→∞.fst(cantor-interval(a;b;f;n)) = x

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  x  :  \mBbbR{}
4.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}n:\mBbbN{}.  (x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))])
6.  a  \mleq{}  b
\mvdash{}  lim  n\mrightarrow{}\minfty{}.fst(cantor-interval(a;b;f;n))  =  x


By

---

Latex:
TACTIC:(InstLemma  `common-limit-squeeze-ext`
                      [\mkleeneopen{}\mlambda{}\msubtwo{}n.fst(cantor-interval(a;b;f;n))\mkleeneclose{}
                      ;  \mkleeneopen{}\mlambda{}\msubtwo{}n.x\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.(2\^{}n  *  b  -  a)/3\^{}n\mkleeneclose{}]\mcdot{}
                THEN  Auto
                THEN  Try  ((BLemma  `cantor-interval-rless`  THEN  Auto))
                THEN  Try  ((BLemma  `cantor-interval-inclusion`\mcdot{}  THEN  Auto))
                THEN  Try  ((D  0  THEN  RWO  "cantor-interval-length"  0  THEN  Auto)))

---

Home Index