---

Step * of Lemma equipollent-nat-rationals

ℕ ~ ℚ
BY
{ xxx(RWO "equipollent-rationals-ext" 0  THEN Auto)xxx }

1
ℕ ~ {p:ℤ × ℕ+| ↑is-qrep(p)} 

---

Latex:

---

Latex:
\mBbbN{}  \msim{}  \mBbbQ{}


By

---

Latex:
xxx(RWO  "equipollent-rationals-ext"  0    THEN  Auto)xxx

---

Home Index