---

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


1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
⊢ ∃k:ℕ. ∀f:ℕn ⟶ 𝔹. G f < k
BY
{ Assert ⌜∃m:ℕ. ℕm ~ ℕn ⟶ 𝔹⌝⋅ }

1
.....assertion..... 
1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
⊢ ∃m:ℕ. ℕm ~ ℕn ⟶ 𝔹

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}m:\mBbbN{}.  \mBbbN{}m  \msim{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}\mkleeneclose{}\mcdot{}

---

Home Index