---

Step * 1 of Lemma cantor-interval-req

.....basecase..... 
1. a : ℝ
2. b : ℝ
3. f : ℕ ⟶ 𝔹
4. n : ℤ
⊢ ((fst(cantor-interval(a;b;f;0))) = (fst(cantor_ivl(a;b;f;0))))
∧ ((snd(cantor-interval(a;b;f;0))) = (snd(cantor_ivl(a;b;f;0))))
BY
{ (D 0
   THEN RepUR ``cantor-interval cantor_ivl unit-interval-fan`` 0
   THEN (Subst' 3^0 ~ 1 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "int-rdiv-req" 0 THEN Auto)
   THEN (RWO "int-rmul-req" 0 THENA Auto)
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
.....basecase..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
4.  n  :  \mBbbZ{}
\mvdash{}  ((fst(cantor-interval(a;b;f;0)))  =  (fst(cantor\_ivl(a;b;f;0))))
\mwedge{}  ((snd(cantor-interval(a;b;f;0)))  =  (snd(cantor\_ivl(a;b;f;0))))


By

---

Latex:
(D  0
  THEN  RepUR  ``cantor-interval  cantor\_ivl  unit-interval-fan``  0
  THEN  (Subst'  3\^{}0  \msim{}  1  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "int-rdiv-req"  0  THEN  Auto)
  THEN  (RWO  "int-rmul-req"  0  THENA  Auto)
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index