---

Step * of Lemma equipollent-rationals

ℚ ~ {p:ℤ × ℕ+| ↑is-qrep(p)} 
BY
{ TACTIC:(TACTIC:With ⌜λr.qrep(r)⌝ (D 0)⋅ THEN Auto) }

1
1. r : ℚ
⊢ qrep(r) ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} 

2
Bij(ℚ;{p:ℤ × ℕ+| ↑is-qrep(p)} ;λr.qrep(r))

---

Latex:

---

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


By

---

Latex:
TACTIC:(TACTIC:With  \mkleeneopen{}\mlambda{}r.qrep(r)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index