---

Step * 1 of Lemma equipollent-rationals


1. r : ℚ
⊢ qrep(r) ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} 
BY
{ ((MemTypeCD THEN Auto) THEN RWO  "assert-is-qrep" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
\mvdash{}  qrep(r)  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  \muparrow{}is-qrep(p)\} 


By

---

Latex:
((MemTypeCD  THEN  Auto)  THEN  RWO    "assert-is-qrep"  0  THEN  Auto)

---

Home Index