---

Step * of Lemma rmax-idempotent

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

---

Latex:

---

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


By

---

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

---

Home Index