---

Step * 1 of Lemma cantor-to-general-cantor


1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. ((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))
6. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
⊢ ∃f:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
   (Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)
   ∧ (∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))))
BY
{ ((Assert ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-}) BY
          (InductionOnNat
           THENL [((InstHyp [⌜0⌝;⌜1⌝] (-1)⋅ THENA Auto) THEN D 0 With ⌜0⌝  THEN Auto)
                 ; (ExRepD
                    THEN ((Decide ⌜k < g (n + 1)⌝⋅ THENA Auto)
                          THENL [D 0 With ⌜n⌝ ; ((Assert g (n + 1) < g ((n + 1) + 1) BY Auto) THEN D 0 With ⌜n + 1⌝ )]
                    )
                    THEN Auto)]
          ))
   THEN (Skolemize (-1) `h' THENA Auto)
   ) }

1
1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. ((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))
6. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
⊢ ∃f:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
   (Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)
   ∧ (∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))))

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  C  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
3.  \mforall{}n:\mBbbN{}.  ((B  n)  \mleq{}  2\^{}(C  n))
4.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
5.  ((g  0)  =  0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  ((g  (i  +  1))  =  ((g  i)  +  (C  i))))
6.  \mforall{}n,m:\mBbbN{}.    (n  <  m  {}\mRightarrow{}  g  n  <  g  m)
\mvdash{}  \mexists{}f:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n]
      (Surj(\mBbbN{}  {}\mrightarrow{}  \mBbbB{};n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n];f)  \mwedge{}  (\mforall{}k:\mBbbN{}.  \mexists{}j:\mBbbN{}.  \mforall{}p,q:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((p  =  q)  {}\mRightarrow{}  ((f  p)  =  (f  q)))))


By

---

Latex:
((Assert  \mforall{}k:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (k  \mmember{}  \{g  n..g  (n  +  1)\msupminus{}\})  BY
                (InductionOnNat
                  THENL  [((InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  D  0  With  \mkleeneopen{}0\mkleeneclose{}    THEN  Auto)
                              ;  (ExRepD
                                    THEN  ((Decide  \mkleeneopen{}k  <  g  (n  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                THENL  [D  0  With  \mkleeneopen{}n\mkleeneclose{} 
                                                            ;  ((Assert  g  (n  +  1)  <  g  ((n  +  1)  +  1)  BY
                                                                                Auto)
                                                                  THEN  D  0  With  \mkleeneopen{}n  +  1\mkleeneclose{} 
                                                                  )]
                                    )
                                    THEN  Auto)]
                ))
  THEN  (Skolemize  (-1)  `h'  THENA  Auto)
  )

---

Home Index