---

Step * 2 of Lemma equipollent-rationals


Bij(ℚ;{p:ℤ × ℕ+| ↑is-qrep(p)} ;λr.qrep(r))
BY
{ (RepeatFor 2 (D 0)
   THEN Reduce 0
   THEN Auto
   THEN Try (((MemTypeCD THEN Auto) THEN RWO  "assert-is-qrep" 0 THEN Auto))) }

1
1. a1 : ℚ
2. a2 : ℚ
3. qrep(a1) = qrep(a2) ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} 
⊢ a1 = a2 ∈ ℚ

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

---

Latex:

---

Latex:

Bij(\mBbbQ{};\{p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}|  \muparrow{}is-qrep(p)\}  ;\mlambda{}r.qrep(r))


By

---

Latex:
(RepeatFor  2  (D  0)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (((MemTypeCD  THEN  Auto)  THEN  RWO    "assert-is-qrep"  0  THEN  Auto)))

---

Home Index