---

Step * 2 2 of Lemma equipollent-rationals


1. b : {p:ℤ × ℕ+| ↑is-qrep(p)} 
⊢ ∃a:ℚ. (qrep(a) = b ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} )
BY
{ TACTIC:TACTIC:Assert ⌜↑is-qrep(b)⌝⋅ }

1
.....assertion..... 
1. b : {p:ℤ × ℕ+| ↑is-qrep(p)} 
⊢ ↑is-qrep(b)

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

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:TACTIC:Assert  \mkleeneopen{}\muparrow{}is-qrep(b)\mkleeneclose{}\mcdot{}

---

Home Index