---

Step * 2 of Lemma rmin_functionality_wrt_rleq


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


By

---

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

---

Home Index