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