---

Step * of Lemma rminus-rmax

∀[x,y:ℝ].  (-(rmax(x;y)) = rmin(-(x);-(y)))
BY
{ (Auto⋅
   THEN D 0
   THEN Auto
   THEN RepUR ``rmin rmax rminus`` 0
   THEN (RWO "imin_unfold imax_unfold" 0 THENA Auto)
   THEN AutoSplit
   THEN (RW IntNormC 0 THEN Auto THEN RWO "absval_unfold" 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    (-(rmax(x;y))  =  rmin(-(x);-(y)))


By

---

Latex:
(Auto\mcdot{}
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``rmin  rmax  rminus``  0
  THEN  (RWO  "imin\_unfold  imax\_unfold"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  (RW  IntNormC  0  THEN  Auto  THEN  RWO  "absval\_unfold"  0  THEN  Auto)\mcdot{})

---

Home Index