---

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


1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
3. m : ℕ
4. g : ℕm ⟶ ℕn ⟶ 𝔹
5. Bij(ℕm;ℕn ⟶ 𝔹;g)
6. v : ℕm ⟶ ℕ
7. (G o g) = v ∈ (ℕm ⟶ ℕ)
⊢ ∃k:ℕ. ∀i:ℕm. v i < k
BY
{ All Thin }

1
1. m : ℕ
2. v : ℕm ⟶ ℕ
⊢ ∃k:ℕ. ∀i:ℕm. v i < k

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  G  :  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}
3.  m  :  \mBbbN{}
4.  g  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}
5.  Bij(\mBbbN{}m;\mBbbN{}n  {}\mrightarrow{}  \mBbbB{};g)
6.  v  :  \mBbbN{}m  {}\mrightarrow{}  \mBbbN{}
7.  (G  o  g)  =  v
\mvdash{}  \mexists{}k:\mBbbN{}.  \mforall{}i:\mBbbN{}m.  v  i  <  k


By

---

Latex:
All  Thin

---

Home Index