---

Step * of Lemma rmin-nonneg

∀[x,y:ℝ].  rnonneg(rmin(x;y)) supposing rnonneg(x) ∧ rnonneg(y)
BY
{ (Auto
   THEN All (Unfold `rnonneg`)
   THEN ParallelLast
   THEN RepUR ``rmin`` 0
   THEN (RWO "imin_unfold" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    rnonneg(rmin(x;y))  supposing  rnonneg(x)  \mwedge{}  rnonneg(y)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `rnonneg`)
  THEN  ParallelLast
  THEN  RepUR  ``rmin``  0
  THEN  (RWO  "imin\_unfold"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index