---

Step * of Lemma rmax_lb

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

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. x ≤ z
5. y ≤ z
⊢ rmax(x;y) ≤ z

---

Latex:

---

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


By

---

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

---

Home Index