---

Step * of Lemma cantor-interval-inclusion2

∀[a,b:ℝ].
  ∀[m:ℕ]. ∀[n:ℕm]. ∀[f:ℕm ⟶ 𝔹].
    (((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))))) 
  supposing a ≤ b
BY
{ (RepeatFor 6 (Intro)
   THEN (InstLemma  `cantor-interval-inclusion` [⌜a⌝;⌜b⌝;⌜λi.if i <z m then f i else ff fi ⌝;⌜n⌝;⌜m⌝]⋅ THENA Auto)
   THEN Repeat (ParallelAnd (-1))
   THEN NthHypEq (-1)
   THEN RepeatFor 3 ((EqCD THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(RepeatFor  6  (Intro)
  THEN  (InstLemma    `cantor-interval-inclusion`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  i  <z  m  then  f  i  else  ff  fi  \mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Repeat  (ParallelAnd  (-1))
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  3  ((EqCD  THEN  Auto)))

---

Home Index