---

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


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
BY
{ ((D 4 With ⌜f1⌝  THENA Auto) THEN D -1) }

1
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

---

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.  Surj(\mBbbN{}  {}\mrightarrow{}  \mBbbB{};n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n];f)
5.  \mforall{}k:\mBbbN{}.  \mexists{}j:\mBbbN{}.  \mforall{}p,q:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((p  =  q)  {}\mRightarrow{}  ((f  p)  =  (f  q)))
6.  B1  :  \mBbbN{}
7.  \mforall{}f@0:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (|F  (f  f@0)|  \mleq{}  B1)
8.  f1  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[n]
\mvdash{}  |F  f1|  \mleq{}  B1


By

---

Latex:
((D  4  With  \mkleeneopen{}f1\mkleeneclose{}    THENA  Auto)  THEN  D  -1)

---

Home Index