---

Step * 2 1 1 1 1 3 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))]
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 ⟶ 𝔹))
12. ∀m:ℕ
      (primrec(m;f;λi,h. (g (n + i) h)) ∈ {f:ℕn + m ⟶ 𝔹| 
                                       x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n + m))]} )
13. λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi 
    ∈ {G:ℕ ⟶ 𝔹| ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} 
⊢ ∃g:ℕ ⟶ 𝔹. ((cantor-to-interval(a;b;g) = x) ∧ (g = f ∈ (ℕn ⟶ 𝔹)))
BY
{ TACTIC:With ⌜λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi ⌝ (D 0)⋅ }

1
.....wf..... 
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 ⟶ 𝔹))
12. ∀m:ℕ
      (primrec(m;f;λi,h. (g (n + i) h)) ∈ {f:ℕn + m ⟶ 𝔹| 
                                       x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n + m))]} )
13. λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi 
    ∈ {G:ℕ ⟶ 𝔹| ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} 
⊢ λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi  ∈ ℕ ⟶ 𝔹

2
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 ⟶ 𝔹))
12. ∀m:ℕ
      (primrec(m;f;λi,h. (g (n + i) h)) ∈ {f:ℕn + m ⟶ 𝔹| 
                                       x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n + m))]} )
13. λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi 
    ∈ {G:ℕ ⟶ 𝔹| ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} 
⊢ (cantor-to-interval(a;b;λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi ) = x)
∧ ((λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi ) = f ∈ (ℕn ⟶ 𝔹))

3
.....wf..... 
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 ⟶ 𝔹))
12. ∀m:ℕ
      (primrec(m;f;λi,h. (g (n + i) h)) ∈ {f:ℕn + m ⟶ 𝔹| 
                                       x ∈ [fst(cantor-interval(a;b;f;n + m)), snd(cantor-interval(a;b;f;n + m))]} )
13. λk.if k <z n then f k else primrec((k - n) + 1;f;λi,h. (g (n + i) h)) k fi 
    ∈ {G:ℕ ⟶ 𝔹| ∀n:ℕ. (x ∈ [fst(cantor-interval(a;b;G;n)), snd(cantor-interval(a;b;G;n))])} 
14. g1 : ℕ ⟶ 𝔹
⊢ istype((cantor-to-interval(a;b;g1) = x) ∧ (g1 = 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))]
9.  \mforall{}n1:\mBbbN{}.  \mforall{}f1:\{f:\mBbbN{}n1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n1)),  snd(cantor-interval(a;b;f;n1))]\}  .
          \mexists{}g:\{g:\mBbbN{}n1  +  1  {}\mrightarrow{}  \mBbbB{}| 
                  x  \mmember{}  [fst(cantor-interval(a;b;g;n1  +  1)),  snd(cantor-interval(a;b;g;n1  +  1))]\} 
            (g  =  f1)
10.  g  :  n1:\mBbbN{}
{}\mrightarrow{}  f1:\{f:\mBbbN{}n1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n1)),  snd(cantor-interval(a;b;f;n1))]\} 
{}\mrightarrow{}  \{g:\mBbbN{}n1  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n1  +  1)),  snd(cantor-interval(a;b;g;n1  +  1))]\} 
11.  \mforall{}n1:\mBbbN{}.  \mforall{}f1:\{f:\mBbbN{}n1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n1)),  snd(cantor-interval(a;b;f;n1))]\}  .
            ((g  n1  f1)  =  f1)
12.  \mforall{}m:\mBbbN{}
            (primrec(m;f;\mlambda{}i,h.  (g  (n  +  i)  h))  \mmember{}  \{f:\mBbbN{}n  +  m  {}\mrightarrow{}  \mBbbB{}| 
                                                                              x  \mmember{}  [fst(cantor-interval(a;b;f;n
                                                                                      +  m)),  snd(cantor-interval(a;b;f;n  +  m))]\}  )
13.  \mlambda{}k.if  k  <z  n  then  f  k  else  primrec((k  -  n)  +  1;f;\mlambda{}i,h.  (g  (n  +  i)  h))  k  fi 
        \mmember{}  \{G:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}|  \mforall{}n:\mBbbN{}.  (x  \mmember{}  [fst(cantor-interval(a;b;G;n)),  snd(cantor-interval(a;b;G;n))])\} 
\mvdash{}  \mexists{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  ((cantor-to-interval(a;b;g)  =  x)  \mwedge{}  (g  =  f))


By

---

Latex:
TACTIC:With  \mkleeneopen{}\mlambda{}k.if  k  <z  n  then  f  k  else  primrec((k  -  n)  +  1;f;\mlambda{}i,h.  (g  (n  +  i)  h))  k  fi  \mkleeneclose{}  (D  0)\mcdot{}

---

Home Index