---

Step * of Lemma cantor-to-interval-req

∀a,b,x:ℝ. ∀f:ℕ ⟶ 𝔹.
  ((∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))])) ⇒ (cantor-to-interval(a;b;f) = x))
BY
{ (Auto
   THEN (Assert a ≤ b BY
               ((InstHyp [⌜0⌝] (-1)⋅ THENA Auto) THEN RepUR ``i-member cantor-interval`` -1 THEN Auto))
   THEN (Assert ⌜lim n→∞.fst(cantor-interval(a;b;f;n)) = x⌝⋅
   THENM ((InstLemma `cantor-to-interval_wf1` [⌜a⌝;⌜b⌝;⌜f⌝]⋅ THENA Auto)
          THEN (MemTypeHD (-1) THENA Auto)
          THEN (Unhide THENA Auto)
          THEN FLemma `unique-limit` [-3;-1]
          THEN Auto)
   )) }

1
.....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

---

Latex:

---

Latex:
\mforall{}a,b,x:\mBbbR{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.
    ((\mforall{}n:\mBbbN{}.  (x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]))
    {}\mRightarrow{}  (cantor-to-interval(a;b;f)  =  x))


By

---

Latex:
(Auto
  THEN  (Assert  a  \mleq{}  b  BY
                          ((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
                            THEN  RepUR  ``i-member  cantor-interval``  -1
                            THEN  Auto))
  THEN  (Assert  \mkleeneopen{}lim  n\mrightarrow{}\minfty{}.fst(cantor-interval(a;b;f;n))  =  x\mkleeneclose{}\mcdot{}
  THENM  ((InstLemma  `cantor-to-interval\_wf1`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (MemTypeHD  (-1)  THENA  Auto)
                THEN  (Unhide  THENA  Auto)
                THEN  FLemma  `unique-limit`  [-3;-1]
                THEN  Auto)
  ))

---

Home Index