---

Step * 1 1 1 1 1 1 1 2 of Lemma countable-Heine-Borel-proper


1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
3. ∃m:ℕ. ℕm ~ ℕn ⟶ 𝔹
⊢ ∃k:ℕ. ∀f:ℕn ⟶ 𝔹. G f < k
BY
{ ExRepD }

1
1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
3. m : ℕ
4. ℕm ~ ℕn ⟶ 𝔹
⊢ ∃k:ℕ. ∀f:ℕn ⟶ 𝔹. G f < k

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  G  :  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}
3.  \mexists{}m:\mBbbN{}.  \mBbbN{}m  \msim{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  G  f  <  k


By

---

Latex:
ExRepD

---

Home Index