---

Step * 1 1 of Lemma rmax-minus-rmin


1. a : ℝ@i
2. b : ℝ@i
⊢ bdd-diff(rmax(a - b;-(a - b));rmax(a;b) - rmin(a;b))
BY
{ (Unfold `rsub` 0
   THEN (RWO "radd-bdd-diff" 0 THENA (Try (Complete (Auto)) THEN (RepUR ``rmax rminus rmin`` 0 THEN Auto)⋅))
   THEN RepUR ``rmax rmin rminus bdd-diff`` 0) }

1
1. a : ℝ@i
2. b : ℝ@i
⊢ ∃B:ℕ. ∀n:ℕ+. (|imax((a n) + (-(b n));-((a n) + (-(b n)))) - imax(a n;b n) + (-imin(a n;b n))| ≤ B)

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}@i
2.  b  :  \mBbbR{}@i
\mvdash{}  bdd-diff(rmax(a  -  b;-(a  -  b));rmax(a;b)  -  rmin(a;b))


By

---

Latex:
(Unfold  `rsub`  0
  THEN  (RWO  "radd-bdd-diff"  0
              THENA  (Try  (Complete  (Auto))  THEN  (RepUR  ``rmax  rminus  rmin``  0  THEN  Auto)\mcdot{})
              )
  THEN  RepUR  ``rmax  rmin  rminus  bdd-diff``  0)

---

Home Index