---

Step * 2 of Lemma rmax_functionality_wrt_rleq


1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. x1 ≤ x2
6. y1 ≤ y2
7. x1 ≤ rmax(x2;y2)
⊢ y1 ≤ rmax(x2;y2)
BY
{ (Assert ⌜y2 ≤ rmax(x2;y2)⌝⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x1  :  \mBbbR{}
2.  x2  :  \mBbbR{}
3.  y1  :  \mBbbR{}
4.  y2  :  \mBbbR{}
5.  x1  \mleq{}  x2
6.  y1  \mleq{}  y2
7.  x1  \mleq{}  rmax(x2;y2)
\mvdash{}  y1  \mleq{}  rmax(x2;y2)


By

---

Latex:
(Assert  \mkleeneopen{}y2  \mleq{}  rmax(x2;y2)\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index