---

Step * 1 of Lemma rmin_functionality_wrt_rleq


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


By

---

Latex:
(Assert  \mkleeneopen{}rmin(x1;y1)  \mleq{}  x1\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index