---

Step * 1 1 1 2 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)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
10. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
11. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
12. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
⊢ ∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((λn.(F n p)) = (λn.(F n q)) ∈ (n:ℕk ⟶ ℕB[n])))
BY
{ ((D 0 THENA Auto)
   THEN (D 0 With ⌜g k⌝  THENW Auto)
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (FunExt THENW Auto)
   THEN Reduce 0) }

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)-})
10. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
11. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
12. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
13. k : ℕ
14. p : ℕ ⟶ 𝔹
15. q : ℕ ⟶ 𝔹
16. p = q ∈ (ℕg k ⟶ 𝔹)
17. n : ℕk
⊢ (F n p) = (F n q) ∈ ℕ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)
7.  \mforall{}k:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (k  \mmember{}  \{g  n..g  (n  +  1)\msupminus{}\})
8.  h  :  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
9.  \mforall{}k:\mBbbN{}.  (k  \mmember{}  \{g  (h  k)..g  ((h  k)  +  1)\msupminus{}\})
10.  \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)
11.  F  :  n:\mBbbN{}  {}\mrightarrow{}  (\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n
12.  \mforall{}n:\mBbbN{}.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;F  n)
\mvdash{}  \mforall{}k:\mBbbN{}.  \mexists{}j:\mBbbN{}.  \mforall{}p,q:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((p  =  q)  {}\mRightarrow{}  ((\mlambda{}n.(F  n  p))  =  (\mlambda{}n.(F  n  q))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (D  0  With  \mkleeneopen{}g  k\mkleeneclose{}    THENW  Auto)
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (FunExt  THENW  Auto)
  THEN  Reduce  0)

---

Home Index