---

Step * of Lemma rmax_functionality_wrt_rleq

∀[x1,x2,y1,y2:ℝ].  (rmax(x1;y1) ≤ rmax(x2;y2)) supposing ((y1 ≤ y2) and (x1 ≤ x2))
BY
{ (Auto THEN BLemma `rmax_lb` THEN Auto) }

1
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. x1 ≤ x2
6. y1 ≤ y2
⊢ x1 ≤ rmax(x2;y2)

2
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. x1 ≤ x2
6. y1 ≤ y2
7. x1 ≤ rmax(x2;y2)
⊢ y1 ≤ rmax(x2;y2)

---

Latex:

---

Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}].    (rmax(x1;y1)  \mleq{}  rmax(x2;y2))  supposing  ((y1  \mleq{}  y2)  and  (x1  \mleq{}  x2))


By

---

Latex:
(Auto  THEN  BLemma  `rmax\_lb`  THEN  Auto)

---

Home Index