---

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

.....assertion..... 
1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
⊢ ∃m:ℕ. ℕm ~ ℕn ⟶ 𝔹
BY
{ ((D 0 With ⌜2^n⌝  THEN Auto) THEN InstLemma `equipollent-powerset` [⌜n⌝;⌜ℕn⌝]⋅ THEN EAuto 1) }

1
1. n : ℕ
2. G : (ℕn ⟶ 𝔹) ⟶ ℕ
3. powerset(ℕn) ~ ℕ2^n
⊢ ℕ2^n ~ ℕn ⟶ 𝔹

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  G  :  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}
\mvdash{}  \mexists{}m:\mBbbN{}.  \mBbbN{}m  \msim{}  \mBbbN{}n  {}\mrightarrow{}  \mBbbB{}


By

---

Latex:
((D  0  With  \mkleeneopen{}2\^{}n\mkleeneclose{}    THEN  Auto)  THEN  InstLemma  `equipollent-powerset`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mBbbN{}n\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index