---

Step * of Lemma cantor_ivl_wf

∀[a,b:ℝ]. ∀[f:ℕ ⟶ 𝔹]. ∀[n:ℕ].  (cantor_ivl(a;b;f;n) ∈ ℝ × ℝ)
BY
{ (ProveWfLemma THEN RWO "exp-fastexp<" 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[n:\mBbbN{}].    (cantor\_ivl(a;b;f;n)  \mmember{}  \mBbbR{}  \mtimes{}  \mBbbR{})


By

---

Latex:
(ProveWfLemma  THEN  RWO  "exp-fastexp<"  0\mcdot{}  THEN  Auto)

---

Home Index