---

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


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 ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
⊢ ∃f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) = x)
BY
{ Assert ⌜λn.(primrec(n + 1;λx.ff;g) n) ∈ {G:ℕ ⟶ 𝔹| 
                                           ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} ⌝\000C⋅ }

1
.....assertion..... 
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 ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
⊢ λn.(primrec(n + 1;λx.ff;g) n) ∈ {G:ℕ ⟶ 𝔹| 
                                   ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} 

2
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 ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ {G:ℕ ⟶ 𝔹| 
                                     ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} 
⊢ ∃f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) = x)

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g)  n)
                \mmember{}  \{G:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}|  \mforall{}n:\mBbbN{}.  (x  \mmember{}  [fst(cantor-interval(a;b;G;n)),  snd(cantor-interval(a;b;G;n))])\}  \mkleeneclose{}\mcdot{}

---

Home Index