---

Step * 1 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))
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))
BY
{ (RepeatFor 2 (MoveToConcl (-3))
   THEN Unfold `so_apply` 0
   THEN Fold `r-ap` 0
   THEN (GenConclTerm ⌜f(x)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜f(y)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜g(x)⌝⋅ THENA Auto)
   THEN (GenConclTerm ⌜g(y)⌝⋅ THENA Auto)
   THEN All Thin)⋅ }

1
1. n : ℕ+
2. v : ℝ
3. v1 : ℝ
4. v2 : ℝ
5. v3 : ℝ
⊢ (|v - v1| ≤ (r1/r(2 * n)))
⇒ (|v2 - v3| ≤ (r1/r(2 * n)))
⇒ ((|(v + v2) - v + v3| + |(v + v3) - v1 + v3|) ≤ (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))
18.  y  \mmember{}  I
19.  x  \mmember{}  I
\mvdash{}  (|(f[x]  +  g[x])  -  f[x]  +  g[y]|  +  |(f[x]  +  g[y])  -  f[y]  +  g[y]|)  \mleq{}  (r1/r(n))


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-3))
  THEN  Unfold  `so\_apply`  0
  THEN  Fold  `r-ap`  0
  THEN  (GenConclTerm  \mkleeneopen{}f(x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}f(y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}g(x)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}g(y)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)\mcdot{}

---

Home Index