---

Step * 1 of Lemma continuous-add


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

1
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. m : {m:ℕ+| icompact(i-approx(I;m))} 
5. n : ℕ+
6. d : ℝ
7. r0 < d
8. d1 : ℝ
9. r0 < d1
10. r0 < rmin(d;d1)
11. x : ℝ
12. y : ℝ
13. x ∈ i-approx(I;m)
14. y ∈ i-approx(I;m)
15. |x - y| ≤ rmin(d;d1)
16. |f[x] - f[y]| ≤ (r1/r(2 * n))
17. |g[x] - g[y]| ≤ (r1/r(2 * n))
18. y ∈ I
19. x ∈ I
⊢ (|(f[x] + g[x]) - f[x] + g[y]| + |(f[x] + g[y]) - f[y] + g[y]|) ≤ (r1/r(n))

---

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))\} 
5.  n  :  \mBbbN{}\msupplus{}
6.  d  :  \mBbbR{}
7.  r0  <  d
8.  d1  :  \mBbbR{}
9.  r0  <  d1
10.  r0  <  rmin(d;d1)
11.  x  :  \mBbbR{}
12.  y  :  \mBbbR{}
13.  x  \mmember{}  i-approx(I;m)
14.  y  \mmember{}  i-approx(I;m)
15.  |x  -  y|  \mleq{}  rmin(d;d1)
16.  |f[x]  -  f[y]|  \mleq{}  (r1/r(2  *  n))
17.  |g[x]  -  g[y]|  \mleq{}  (r1/r(2  *  n))
\mvdash{}  |(f[x]  +  g[x])  -  f[y]  +  g[y]|  \mleq{}  (r1/r(n))


By

---

Latex:
(\mforall{}h:hyp.  (FLemma  `i-member-approx`  [h]  THENA  Complete  (Auto)) 
  THEN  UseTriangleInequality  [\mkleeneopen{}f[x]  +  g[y]\mkleeneclose{}]\mcdot{}
  )

---

Home Index