---

Step * of Lemma rmin-rleq

∀[x,y:ℝ].  ((rmin(x;y) ≤ x) ∧ (rmin(x;y) ≤ y))
BY
{ (Auto
   THEN (RWO "rmin-req-rminus-rmax" 0 THENA Auto)
   THEN RW (AddrC [2] (RevLemmaC `rminus-rminus`)) 0
   THEN Auto
   THEN BLemma `rminus_functionality_wrt_rleq`
   THEN Auto
   THEN Unfold `rge` 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWO  "rmin-req-rminus-rmax"  0  THENA  Auto)
  THEN  RW  (AddrC  [2]  (RevLemmaC  `rminus-rminus`))  0
  THEN  Auto
  THEN  BLemma  `rminus\_functionality\_wrt\_rleq`
  THEN  Auto
  THEN  Unfold  `rge`  0
  THEN  Auto)

---

Home Index