---

Step * of Lemma rmin-idempotent

∀[x:ℝ]. (rmin(x;x) = x)
BY
{ (Auto THEN Assert ⌜(rmin(x;x) ≤ x) ∧ (x ≤ rmin(x;x))⌝⋅ THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}(rmin(x;x)  \mleq{}  x)  \mwedge{}  (x  \mleq{}  rmin(x;x))\mkleeneclose{}\mcdot{}  THEN  EAuto  1)

---

Home Index