---

Step * 2 2 2 of Lemma equipollent-rationals


1. b : {p:ℤ × ℕ+| ↑is-qrep(p)} 
2. ↑is-qrep(b)
⊢ ∃a:ℚ. (qrep(a) = b ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} )
BY
{ (RWO "assert-is-qrep" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \{p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  \muparrow{}is-qrep(p)\} 
2.  \muparrow{}is-qrep(b)
\mvdash{}  \mexists{}a:\mBbbQ{}.  (qrep(a)  =  b)


By

---

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

---

Home Index