---

Step * 1 of Lemma in-rat-cube-intersection


1. v5 : ℚ
2. v6 : ℚ
3. v3 : ℚ
4. v4 : ℚ
5. v2 : ℝ
6. rat2real(v3) ≤ v2
7. v2 ≤ rat2real(v4)
8. rat2real(v5) ≤ v2
9. v2 ≤ rat2real(v6)
⊢ rat2real(qmax(v5;v3)) ≤ v2
BY
{ ((RWO "rat2real-qmax" 0 THENM BLemma `rmax_lb`) THEN Auto) }

---

Latex:

---

Latex:

1.  v5  :  \mBbbQ{}
2.  v6  :  \mBbbQ{}
3.  v3  :  \mBbbQ{}
4.  v4  :  \mBbbQ{}
5.  v2  :  \mBbbR{}
6.  rat2real(v3)  \mleq{}  v2
7.  v2  \mleq{}  rat2real(v4)
8.  rat2real(v5)  \mleq{}  v2
9.  v2  \mleq{}  rat2real(v6)
\mvdash{}  rat2real(qmax(v5;v3))  \mleq{}  v2


By

---

Latex:
((RWO  "rat2real-qmax"  0  THENM  BLemma  `rmax\_lb`)  THEN  Auto)

---

Home Index