---

Step * of Lemma rmin_wf

∀[x,y:ℝ].  (rmin(x;y) ∈ ℝ)
BY
{ (ProveWfLemma
   THEN D 1
   THEN D -1
   THEN (MemTypeCD THEN Auto)
   THEN All (Unfold `regular-int-seq`)
   THEN Reduce 0
   THEN Auto
   THEN (RWO "mul-imin" 0 THEN Auto THEN (RWO "absval-imin-difference" 0 THENA Auto) THEN BLemma `imax_lb` THEN Auto)
   ⋅) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma
  THEN  D  1
  THEN  D  -1
  THEN  (MemTypeCD  THEN  Auto)
  THEN  All  (Unfold  `regular-int-seq`)
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "mul-imin"  0
              THEN  Auto
              THEN  (RWO  "absval-imin-difference"  0  THENA  Auto)
              THEN  BLemma  `imax\_lb`
              THEN  Auto)\mcdot{})

---

Home Index