---

Step * 2 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)
10. rat2real(qmax(v5;v3)) ≤ v2
⊢ v2 ≤ rat2real(qmin(v6;v4))
BY
{ ((RWO "rat2real-qmin" 0 THENM BLemma `rmin_ub`) 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)
10.  rat2real(qmax(v5;v3))  \mleq{}  v2
\mvdash{}  v2  \mleq{}  rat2real(qmin(v6;v4))


By

---

Latex:
((RWO  "rat2real-qmin"  0  THENM  BLemma  `rmin\_ub`)  THEN  Auto)

---

Home Index