---

Step * 1 of Lemma rmin_ub


1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. z ≤ x@i
5. z ≤ y@i
⊢ z ≤ rmin(x;y)
BY
{ (All (Unfold `rleq`) THEN All (Unfold `rsub`)) }

1
1. x : ℝ@i
2. y : ℝ@i
3. z : ℝ@i
4. rnonneg(x + -(z))@i
5. rnonneg(y + -(z))@i
⊢ rnonneg(rmin(x;y) + -(z))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
3.  z  :  \mBbbR{}@i
4.  z  \mleq{}  x@i
5.  z  \mleq{}  y@i
\mvdash{}  z  \mleq{}  rmin(x;y)


By

---

Latex:
(All  (Unfold  `rleq`)  THEN  All  (Unfold  `rsub`))

---

Home Index