---

Step * of Lemma rmin_functionality_wrt_rleq

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

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `rmin\_ub`  THEN  Auto)

---

Home Index