---

Step * 1 of Lemma rleq-rmax

.....assertion..... 
∀x,y:ℝ.  (x ≤ rmax(x;y))
BY
{ (Auto THEN Unfold `rleq` 0 THEN Unfold `rnonneg` 0 THEN Auto THEN RepUR ``rmax rsub radd rminus accelerate`` 0) }

1
1. x : ℝ
2. y : ℝ
3. n : ℕ+
⊢ (-2) ≤ eval m = 4 * n in
         (reg-seq-list-add([λn.imax(x n;y n); λn.(-(x n))]) m) ÷ 4

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}x,y:\mBbbR{}.    (x  \mleq{}  rmax(x;y))


By

---

Latex:
(Auto
  THEN  Unfold  `rleq`  0
  THEN  Unfold  `rnonneg`  0
  THEN  Auto
  THEN  RepUR  ``rmax  rsub  radd  rminus  accelerate``  0)

---

Home Index