---

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


1. B : ℕ ⟶ ℕ+
2. F : (n:ℕ ⟶ ℕB[n]) ⟶ ℤ
3. f : (ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕB[n]
4. ∀k:ℕ. ∃j:ℕ. ∀p,q:ℕ ⟶ 𝔹.  ((p = q ∈ (ℕj ⟶ 𝔹)) ⇒ ((f p) = (f q) ∈ (n:ℕk ⟶ ℕB[n])))
5. B1 : ℕ
6. ∀f@0:ℕ ⟶ 𝔹. (|F (f f@0)| ≤ B1)
7. f1 : n:ℕ ⟶ ℕB[n]
8. a : ℕ ⟶ 𝔹
9. (f a) = f1 ∈ (n:ℕ ⟶ ℕB[n])
⊢ |F f1| ≤ B1
BY
{ (D -4 With ⌜a⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n])  {}\mrightarrow{}  \mBbbZ{}
3.  f  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n]
4.  \mforall{}k:\mBbbN{}.  \mexists{}j:\mBbbN{}.  \mforall{}p,q:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((p  =  q)  {}\mRightarrow{}  ((f  p)  =  (f  q)))
5.  B1  :  \mBbbN{}
6.  \mforall{}f@0:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (|F  (f  f@0)|  \mleq{}  B1)
7.  f1  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n]
8.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
9.  (f  a)  =  f1
\mvdash{}  |F  f1|  \mleq{}  B1


By

---

Latex:
(D  -4  With  \mkleeneopen{}a\mkleeneclose{}    THEN  Auto)

---

Home Index