---

Step * of Lemma rmin-req

∀[x,y:ℝ].  rmin(x;y) = y supposing y ≤ x
BY
{ (Auto THEN InstLemma `rmax-req` [⌜-(x)⌝;⌜-(y)⌝]⋅ THEN EAuto 1) }

1
1. x : ℝ
2. y : ℝ
3. y ≤ x
4. rmax(-(x);-(y)) = -(y)
⊢ rmin(x;y) = y

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  InstLemma  `rmax-req`  [\mkleeneopen{}-(x)\mkleeneclose{};\mkleeneopen{}-(y)\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index