---

Step * 2 1 1 2 of Lemma cantor-to-interval-onto-common


1. a : ℝ
2. b : ℝ
3. [%] : a < b
4. x : ℝ
5. x ∈ [a, b]
6. n : ℕ
7. f : ℕn ⟶ 𝔹
8. x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]
⊢ ∃g:ℕ ⟶ 𝔹. ((cantor-to-interval(a;b;g) = x) ∧ (g = f ∈ (ℕn ⟶ 𝔹)))
BY
{ ((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. x ∈ [a, b]
6. n : ℕ
7. f : ℕn ⟶ 𝔹
8. x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]
9. ∀n1:ℕ. ∀f1:{f:ℕn1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n1)), snd(cantor-interval(a;b;f;n1))]} .
     ∃g:{g:ℕn1 + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n1 + 1)), snd(cantor-interval(a;b;g;n1 + 1))]} 
      (g = f1 ∈ (ℕn1 ⟶ 𝔹))
10. g : n1:ℕ
⟶ f1:{f:ℕn1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n1)), snd(cantor-interval(a;b;f;n1))]} 
⟶ {g:ℕn1 + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n1 + 1)), snd(cantor-interval(a;b;g;n1 + 1))]} 
11. ∀n1:ℕ. ∀f1:{f:ℕn1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n1)), snd(cantor-interval(a;b;f;n1))]} .
      ((g n1 f1) = f1 ∈ (ℕn1 ⟶ 𝔹))
⊢ ∃g:ℕ ⟶ 𝔹. ((cantor-to-interval(a;b;g) = x) ∧ (g = f ∈ (ℕn ⟶ 𝔹)))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  [\%]  :  a  <  b
4.  x  :  \mBbbR{}
5.  x  \mmember{}  [a,  b]
6.  n  :  \mBbbN{}
7.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
8.  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]
\mvdash{}  \mexists{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((cantor-to-interval(a;b;g)  =  x)  \mwedge{}  (g  =  f))


By

---

Latex:
((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