---

Step * 1 of Lemma continuous-max


1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} @i
5. n : ℕ+@i
6. d : ℝ
7. r0 < d
8. d1 : ℝ
9. r0 < d1
10. r0 < rmin(d;d1)
11. x : ℝ@i
12. y : ℝ@i
13. x ∈ i-approx(I;m)@i
14. y ∈ i-approx(I;m)@i
15. |x - y| ≤ rmin(d;d1)@i
16. |f[x] - f[y]| ≤ (r1/r(n))
17. |g[x] - g[y]| ≤ (r1/r(n))
⊢ |rmax(f[x];g[x]) - rmax(f[y];g[y])| ≤ (r1/r(n))
BY
{ (∀h:hyp. (FLemma `i-member-approx` [h] THENA Complete (Auto)) 
   THEN RWO "rabs-difference-rmax" 0
   THEN Auto
   THEN BLemma `rmax_lb` 
   THEN Auto) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  f  :  I  {}\mrightarrow{}\mBbbR{}
3.  g  :  I  {}\mrightarrow{}\mBbbR{}
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  @i
5.  n  :  \mBbbN{}\msupplus{}@i
6.  d  :  \mBbbR{}
7.  r0  <  d
8.  d1  :  \mBbbR{}
9.  r0  <  d1
10.  r0  <  rmin(d;d1)
11.  x  :  \mBbbR{}@i
12.  y  :  \mBbbR{}@i
13.  x  \mmember{}  i-approx(I;m)@i
14.  y  \mmember{}  i-approx(I;m)@i
15.  |x  -  y|  \mleq{}  rmin(d;d1)@i
16.  |f[x]  -  f[y]|  \mleq{}  (r1/r(n))
17.  |g[x]  -  g[y]|  \mleq{}  (r1/r(n))
\mvdash{}  |rmax(f[x];g[x])  -  rmax(f[y];g[y])|  \mleq{}  (r1/r(n))


By

---

Latex:
(\mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THENA  Complete  (Auto)) 
  THEN  RWO  "rabs-difference-rmax"  0
  THEN  Auto
  THEN  BLemma  `rmax\_lb` 
  THEN  Auto)

---

Home Index