---

Step * 1 of Lemma req-rat2real


1. q1 : ℚ
2. q2 : ℚ
3. rat2real(q1) = rat2real(q2)
⊢ q1 = q2 ∈ ℚ
BY
{ (SupposeNot THEN (RWO "rneq-rat2real<" (-1) THENA Auto)) }

1
1. q1 : ℚ
2. q2 : ℚ
3. rat2real(q1) = rat2real(q2)
4. rat2real(q1) ≠ rat2real(q2)
⊢ q1 = q2 ∈ ℚ

---

Latex:

---

Latex:

1.  q1  :  \mBbbQ{}
2.  q2  :  \mBbbQ{}
3.  rat2real(q1)  =  rat2real(q2)
\mvdash{}  q1  =  q2


By

---

Latex:
(SupposeNot  THEN  (RWO  "rneq-rat2real<"  (-1)  THENA  Auto))

---

Home Index