---

Step * 1 of Lemma rabs-difference-rmax


1. a : ℝ
2. b : ℝ
3. x : ℝ
4. y : ℝ
⊢ rnonneg2(rmax(|x - a|;|y - b|) - |rmax(x;y) - rmax(a;b)|)
BY
{ (Unfold `rsub` 0
   THEN (RWO "radd-bdd-diff" 0 THENA Auto)
   THEN Fold `reg-seq-add` 0
   THEN (RWO "radd-bdd-diff" 0
         THENA (Try (Complete (Auto)) THEN Try (Complete ((RepUR ``rabs rmax rminus`` 0 THEN Auto))))
         )
   THEN RepUR ``reg-seq-add rmax rabs rminus`` 0) }

1
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. y : ℝ
⊢ rnonneg2(λn.(imax(|(x n) + (-(a n))|;|(y n) + (-(b n))|) + (-|imax(x n;y n) + (-imax(a n;b n))|)))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  x  :  \mBbbR{}
4.  y  :  \mBbbR{}
\mvdash{}  rnonneg2(rmax(|x  -  a|;|y  -  b|)  -  |rmax(x;y)  -  rmax(a;b)|)


By

---

Latex:
(Unfold  `rsub`  0
  THEN  (RWO  "radd-bdd-diff"  0  THENA  Auto)
  THEN  Fold  `reg-seq-add`  0
  THEN  (RWO  "radd-bdd-diff"  0
              THENA  (Try  (Complete  (Auto))  THEN  Try  (Complete  ((RepUR  ``rabs  rmax  rminus``  0  THEN  Auto))))
              )
  THEN  RepUR  ``reg-seq-add  rmax  rabs  rminus``  0)

---

Home Index