---

Step * of Lemma cantor-to-interval_wf

∀a,b:ℝ.  ∀f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) ∈ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} ) supposing a ≤ b
BY
{ (Auto THEN DoSubsume) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : ℕ ⟶ 𝔹
⊢ cantor-to-interval(a;b;f) ∈ {x:ℝ| lim n→∞.fst(cantor-interval(a;b;f;n)) = x} 

2
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. f : ℕ ⟶ 𝔹
5. cantor-to-interval(a;b;f) = cantor-to-interval(a;b;f) ∈ {x:ℝ| lim n→∞.fst(cantor-interval(a;b;f;n)) = x} 
⊢ {x:ℝ| lim n→∞.fst(cantor-interval(a;b;f;n)) = x}  ⊆r {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (cantor-to-interval(a;b;f)  \mmember{}  \{x:\mBbbR{}|  (a  \mleq{}  x)  \mwedge{}  (x  \mleq{}  b)\}  )  supposing  a  \mleq{}  b


By

---

Latex:
(Auto  THEN  DoSubsume)

---

Home Index