---

Step * of Lemma rmax_ub

∀[x,y,z:ℝ].  z ≤ rmax(x;y) supposing (z ≤ x) ∨ (z ≤ y)
BY
{ (Auto THEN ((InstLemma `rleq-rmax` [⌜x⌝; ⌜y⌝])⋅ THENA Auto) THEN D -2 THEN D -1 THEN RelRST THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    z  \mleq{}  rmax(x;y)  supposing  (z  \mleq{}  x)  \mvee{}  (z  \mleq{}  y)


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rleq-rmax`  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  D  -1
  THEN  RelRST
  THEN  Auto)

---

Home Index