---

Step * of Lemma equipollent-rationals-ext

ℚ ~ {p:ℤ × ℕ+| ↑is-qrep(p)} 
BY
{ xxxExtract of Obid: equipollent-rationals
     not unfolding  qrep
     finishing with Auto
     normalizes to:
     
     <λr.qrep(r), λa1,a2,%. Ax, λb.<b, Ax>>xxx }

---

Latex:

---

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


By

---

Latex:
xxxExtract  of  Obid:  equipollent-rationals
      not  unfolding    qrep
      finishing  with  Auto
      normalizes  to:
     
      <\mlambda{}r.qrep(r),  \mlambda{}a1,a2,\%.  Ax,  \mlambda{}b.<b,  Ax>>xxx

---

Home Index