---

Step * of Lemma cantor-interval-cauchy

∀a,b:ℝ.  ∀[f:ℕ ⟶ 𝔹]. cauchy(n.fst(cantor-interval(a;b;f;n))) supposing a ≤ b
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (InstLemma `cantor-interval-inclusion` [⌜a⌝;⌜b⌝;⌜f⌝]⋅ THENA Auto)
   THEN (InstLemma `cantor-interval-length` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN ((Assert ⌜∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ ((2^n * b - a)/3^n ≤ (r1/r(k)))))]⌝⋅
         THENM (RepeatFor 2 (ParallelLast) THEN Auto)
         )
         THENA ThinVar `f'
         )) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. k : ℕ+
5. ∀[n:ℕ]. ∀[f:ℕn ⟶ 𝔹].  (((snd(cantor-interval(a;b;f;n))) - fst(cantor-interval(a;b;f;n))) = (2^n * b - a)/3^n)
⊢ ∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ ((2^n * b - a)/3^n ≤ (r1/r(k)))))]

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : ℕ ⟶ 𝔹
5. k : ℕ+
6. ∀[n:ℕ]. ∀[m:{n...}].
     (((fst(cantor-interval(a;b;f;n))) ≤ (fst(cantor-interval(a;b;f;m))))
     ∧ ((fst(cantor-interval(a;b;f;m))) ≤ (snd(cantor-interval(a;b;f;m))))
     ∧ ((snd(cantor-interval(a;b;f;m))) ≤ (snd(cantor-interval(a;b;f;n)))))
7. ∀[n:ℕ]. ∀[f:ℕn ⟶ 𝔹].  (((snd(cantor-interval(a;b;f;n))) - fst(cantor-interval(a;b;f;n))) = (2^n * b - a)/3^n)
8. N : ℕ
9. ∀n:ℕ. ((N ≤ n) ⇒ ((2^n * b - a)/3^n ≤ (r1/r(k))))
10. n : ℕ
11. m : ℕ
12. N ≤ n
13. N ≤ m
14. (2^n * b - a)/3^n ≤ (r1/r(k))
⊢ |(fst(cantor-interval(a;b;f;n))) - fst(cantor-interval(a;b;f;m))| ≤ (r1/r(k))

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  cauchy(n.fst(cantor-interval(a;b;f;n)))  supposing  a  \mleq{}  b


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `cantor-interval-inclusion`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `cantor-interval-length`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((Assert  \mkleeneopen{}\mexists{}N:\mBbbN{}  [(\mforall{}n:\mBbbN{}.  ((N  \mleq{}  n)  {}\mRightarrow{}  ((2\^{}n  *  b  -  a)/3\^{}n  \mleq{}  (r1/r(k)))))]\mkleeneclose{}\mcdot{}
              THENM  (RepeatFor  2  (ParallelLast)  THEN  Auto)
              )
              THENA  ThinVar  `f'
              ))

---

Home Index