---

Step * 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 ⟶ 𝔹))
⊢ ∃f:ℕ ⟶ 𝔹. (cantor-to-interval(a;b;f) = x)
BY
{ (Assert ⌜∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )\000C⌝⋅
   THENA ((D 0 THENA Auto)
          THEN InstLemma `primrec-wf` [⌜λ2n.{f:ℕn ⟶ 𝔹| 
                                             x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} ⌝
          ; ⌜λi.ff⌝;⌜g⌝;⌜n⌝]⋅
          THEN 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 ⟶ 𝔹))
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)

---

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)
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (cantor-to-interval(a;b;f)  =  x)


By

---

Latex:
(Assert  \mkleeneopen{}\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))]\}  \000C)\mkleeneclose{}\mcdot{}
  THENA  ((D  0  THENA  Auto)
                THEN  InstLemma  `primrec-wf`  [
                \mkleeneopen{}\mlambda{}\msubtwo{}n.\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  \mkleeneclose{}
                ;  \mkleeneopen{}\mlambda{}i.ff\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
                THEN  Auto)
  )

---

Home Index