---

Step * of Lemma general-cantor-to-int-bounded

∀B:ℕ ⟶ ℕ+. ∀F:(n:ℕ ⟶ ℕB[n]) ⟶ ℤ.  ∃bnd:ℕ. ∀f:n:ℕ ⟶ ℕB[n]. (|F f| ≤ bnd)
BY
{ (Auto
   THEN (InstLemma `cantor-to-general-cantor` [⌜B⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstLemma `cantor-to-int-bounded` [⌜F o f⌝]⋅ THENA Auto)
   THEN (ParallelLast THEN RepUR ``compose`` -1)
   THEN (D 0 THENA Auto)) }

1
1. B : ℕ ⟶ ℕ+
2. F : (n:ℕ ⟶ ℕB[n]) ⟶ ℤ
3. f : (ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
4. Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕB[n];f)
5. ∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))
6. B1 : ℕ
7. ∀f@0:ℕ ⟶ 𝔹. (|F (f f@0)| ≤ B1)
8. f1 : n:ℕ ⟶ ℕB[n]
⊢ |F f1| ≤ B1

---

Latex:

---

Latex:
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mforall{}F:(n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n])  {}\mrightarrow{}  \mBbbZ{}.    \mexists{}bnd:\mBbbN{}.  \mforall{}f:n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n].  (|F  f|  \mleq{}  bnd)


By

---

Latex:
(Auto
  THEN  (InstLemma  `cantor-to-general-cantor`  [\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `cantor-to-int-bounded`  [\mkleeneopen{}F  o  f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ParallelLast  THEN  RepUR  ``compose``  -1)
  THEN  (D  0  THENA  Auto))

---

Home Index