---

Step * 1 of Lemma equipollent-nat-rationals


ℕ ~ {p:ℤ × ℕ+| ↑is-qrep(p)} 
BY
{ (BLemma `equipollent-nat-subset-ext` THEN Auto) }

1
1. L : (ℤ × ℕ+) List
⊢ ∃p:ℤ × ℕ+. ((↑is-qrep(p)) ∧ (¬(p ∈ L)))

2
ℕ ~ ℤ × ℕ+

---

Latex:

---

Latex:

\mBbbN{}  \msim{}  \{p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  \muparrow{}is-qrep(p)\} 


By

---

Latex:
(BLemma  `equipollent-nat-subset-ext`  THEN  Auto)

---

Home Index