---

Step * of Lemma cantor-to-interval-onto-proper

∀a,b:ℝ.  ∀x:ℝ. ((a ≤ x) ⇒ (x ≤ b) ⇒ (∃f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) = x))) supposing a < b
BY
{ (Auto
   THEN (InstLemma `cantor-to-interval-onto-lemma` [⌜a⌝;⌜b⌝;⌜x⌝]⋅ THENA Auto)
   THEN (Skolemize (-1) `g'  THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
     ∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} 
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} 
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .  ((g n f) = f ∈ (ℕn ⟶ 𝔹))
⊢ ∃f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) = x)

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    \mforall{}x:\mBbbR{}.  ((a  \mleq{}  x)  {}\mRightarrow{}  (x  \mleq{}  b)  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (cantor-to-interval(a;b;f)  =  x)))  supposing  a  <  b


By

---

Latex:
(Auto
  THEN  (InstLemma  `cantor-to-interval-onto-lemma`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Skolemize  (-1)  `g'    THENA  Auto))

---

Home Index