---

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


1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. (g 0) = 0 ∈ ℤ
6. ∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ)
7. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
8. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
9. h : k:ℕ ⟶ ℕ
10. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
11. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
12. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
13. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
14. k : ℕ
15. p : ℕ ⟶ 𝔹
16. q : ℕ ⟶ 𝔹
17. p = q ∈ (ℕg k ⟶ 𝔹)
18. n : ℕk
19. p = q ∈ (ℕg k ⟶ 𝔹)
⊢ (g (n + 1)) ≤ (g k)
BY
{ (Decide ⌜n + 1 < k⌝⋅ THEN Auto THEN Subst' n + 1 ~ k 0 THEN Auto) }

---

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
6.  \mforall{}i:\mBbbN{}.  ((g  (i  +  1))  =  ((g  i)  +  (C  i)))
7.  \mforall{}n,m:\mBbbN{}.    (n  <  m  {}\mRightarrow{}  g  n  <  g  m)
8.  \mforall{}k:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (k  \mmember{}  \{g  n..g  (n  +  1)\msupminus{}\})
9.  h  :  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
10.  \mforall{}k:\mBbbN{}.  (k  \mmember{}  \{g  (h  k)..g  ((h  k)  +  1)\msupminus{}\})
11.  \mforall{}n:\mBbbN{}.  \mexists{}f:(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;f)
12.  F  :  n:\mBbbN{}  {}\mrightarrow{}  (\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n
13.  \mforall{}n:\mBbbN{}.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;F  n)
14.  k  :  \mBbbN{}
15.  p  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
16.  q  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
17.  p  =  q
18.  n  :  \mBbbN{}k
19.  p  =  q
\mvdash{}  (g  (n  +  1))  \mleq{}  (g  k)


By

---

Latex:
(Decide  \mkleeneopen{}n  +  1  <  k\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  Subst'  n  +  1  \msim{}  k  0  THEN  Auto)

---

Home Index