---

Step * of Lemma rmax_functionality

∀[x1,x2,y1,y2:ℝ].  (rmax(x1;y1) = rmax(x2;y2)) supposing ((x1 = x2) and (y1 = y2))
BY
{ (Auto THEN All (RWO "req-iff-bdd-diff" )⋅ THEN Auto) }

1
1. x1 : ℝ
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. bdd-diff(y1;y2)
6. bdd-diff(x1;x2)
⊢ bdd-diff(rmax(x1;y1);rmax(x2;y2))

---

Latex:

---

Latex:
\mforall{}[x1,x2,y1,y2:\mBbbR{}].    (rmax(x1;y1)  =  rmax(x2;y2))  supposing  ((x1  =  x2)  and  (y1  =  y2))


By

---

Latex:
(Auto  THEN  All  (RWO  "req-iff-bdd-diff"  )\mcdot{}  THEN  Auto)

---

Home Index