---

Step * 1 of Lemma rmax_functionality_wrt_rleq


1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. x1 ≤ x2
6. y1 ≤ y2
⊢ x1 ≤ rmax(x2;y2)
BY
{ (Assert ⌜x2 ≤ 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
\mvdash{}  x1  \mleq{}  rmax(x2;y2)


By

---

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

---

Home Index