---

Step * of Lemma cantor-to-int-bounded

∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ∃B:ℕ. ∀f:ℕ ⟶ 𝔹. (|F f| ≤ B)
BY
{ (InstLemma `cantor-to-int-uniform-continuity` [] THEN ParallelLast' THEN D -1) }

1
1. F : (ℕ ⟶ 𝔹) ⟶ ℤ
2. n : ℕ
3. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℤ))
⊢ ∃B:ℕ. ∀f:ℕ ⟶ 𝔹. (|F f| ≤ B)

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbZ{}.  \mexists{}B:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (|F  f|  \mleq{}  B)


By

---

Latex:
(InstLemma  `cantor-to-int-uniform-continuity`  []  THEN  ParallelLast'  THEN  D  -1)

---

Home Index