Step
*
2
1
2
1
1
of Lemma
continuous-mul
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. rmax(|f[x]|;|g[x]|) continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))}
6. n : ℕ+
7. N : ℕ+
8. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
9. f ∈ i-approx(I;m) ⟶ℝ
10. g ∈ i-approx(I;m) ⟶ℝ
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * n) * N))))
14. d1 : ℝ
15. r0 < d1
16. ∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|g[x] - g[y]| ≤ (r1/r((2 * n) * N))))
17. r0 < rmin(d;d1)
18. x : ℝ
19. y : ℝ
20. x ∈ i-approx(I;m)
21. y ∈ i-approx(I;m)
22. |x - y| ≤ rmin(d;d1)
23. r0 ≤ |g[y]|
24. |(f[x] - f[y]) * g[y]| ≤ ((r1/r((2 * n) * N)) * |g[y]|)
25. r0 ≤ |f[x]|
26. |(g[x] - g[y]) * f[x]| ≤ ((r1/r((2 * n) * N)) * |f[x]|)
⊢ (|f[x] * (g[x] - g[y])| + |(f[x] - f[y]) * g[y]|) ≤ (r1/r(n))
BY
{ Assert ⌜(|f[x]| ≤ r(N)) ∧ (|g[y]| ≤ r(N))⌝⋅ }
1
.....assertion.....
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. rmax(|f[x]|;|g[x]|) continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))}
6. n : ℕ+
7. N : ℕ+
8. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
9. f ∈ i-approx(I;m) ⟶ℝ
10. g ∈ i-approx(I;m) ⟶ℝ
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * n) * N))))
14. d1 : ℝ
15. r0 < d1
16. ∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|g[x] - g[y]| ≤ (r1/r((2 * n) * N))))
17. r0 < rmin(d;d1)
18. x : ℝ
19. y : ℝ
20. x ∈ i-approx(I;m)
21. y ∈ i-approx(I;m)
22. |x - y| ≤ rmin(d;d1)
23. r0 ≤ |g[y]|
24. |(f[x] - f[y]) * g[y]| ≤ ((r1/r((2 * n) * N)) * |g[y]|)
25. r0 ≤ |f[x]|
26. |(g[x] - g[y]) * f[x]| ≤ ((r1/r((2 * n) * N)) * |f[x]|)
⊢ (|f[x]| ≤ r(N)) ∧ (|g[y]| ≤ r(N))
2
1. I : Interval
2. f : I ⟶ℝ
3. g : I ⟶ℝ
4. rmax(|f[x]|;|g[x]|) continuous for x ∈ I
5. m : {m:ℕ+| icompact(i-approx(I;m))}
6. n : ℕ+
7. N : ℕ+
8. ∀[x:{r:ℝ| r ∈ i-approx(I;m)} ]. (rmax(|f[x]|;|g[x]|) ≤ r(N))
9. f ∈ i-approx(I;m) ⟶ℝ
10. g ∈ i-approx(I;m) ⟶ℝ
11. d : ℝ
12. r0 < d
13. ∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r((2 * n) * N))))
14. d1 : ℝ
15. r0 < d1
16. ∀x,y:ℝ. ((x ∈ i-approx(I;m)) ⇒ (y ∈ i-approx(I;m)) ⇒ (|x - y| ≤ d1) ⇒ (|g[x] - g[y]| ≤ (r1/r((2 * n) * N))))
17. r0 < rmin(d;d1)
18. x : ℝ
19. y : ℝ
20. x ∈ i-approx(I;m)
21. y ∈ i-approx(I;m)
22. |x - y| ≤ rmin(d;d1)
23. r0 ≤ |g[y]|
24. |(f[x] - f[y]) * g[y]| ≤ ((r1/r((2 * n) * N)) * |g[y]|)
25. r0 ≤ |f[x]|
26. |(g[x] - g[y]) * f[x]| ≤ ((r1/r((2 * n) * N)) * |f[x]|)
27. (|f[x]| ≤ r(N)) ∧ (|g[y]| ≤ r(N))
⊢ (|f[x] * (g[x] - g[y])| + |(f[x] - f[y]) * g[y]|) ≤ (r1/r(n))
Latex:
Latex:
1. I : Interval
2. f : I {}\mrightarrow{}\mBbbR{}
3. g : I {}\mrightarrow{}\mBbbR{}
4. rmax(|f[x]|;|g[x]|) continuous for x \mmember{} I
5. m : \{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m))\}
6. n : \mBbbN{}\msupplus{}
7. N : \mBbbN{}\msupplus{}
8. \mforall{}[x:\{r:\mBbbR{}| r \mmember{} i-approx(I;m)\} ]. (rmax(|f[x]|;|g[x]|) \mleq{} r(N))
9. f \mmember{} i-approx(I;m) {}\mrightarrow{}\mBbbR{}
10. g \mmember{} i-approx(I;m) {}\mrightarrow{}\mBbbR{}
11. d : \mBbbR{}
12. r0 < d
13. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;m))
{}\mRightarrow{} (y \mmember{} i-approx(I;m))
{}\mRightarrow{} (|x - y| \mleq{} d)
{}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r1/r((2 * n) * N))))
14. d1 : \mBbbR{}
15. r0 < d1
16. \mforall{}x,y:\mBbbR{}.
((x \mmember{} i-approx(I;m))
{}\mRightarrow{} (y \mmember{} i-approx(I;m))
{}\mRightarrow{} (|x - y| \mleq{} d1)
{}\mRightarrow{} (|g[x] - g[y]| \mleq{} (r1/r((2 * n) * N))))
17. r0 < rmin(d;d1)
18. x : \mBbbR{}
19. y : \mBbbR{}
20. x \mmember{} i-approx(I;m)
21. y \mmember{} i-approx(I;m)
22. |x - y| \mleq{} rmin(d;d1)
23. r0 \mleq{} |g[y]|
24. |(f[x] - f[y]) * g[y]| \mleq{} ((r1/r((2 * n) * N)) * |g[y]|)
25. r0 \mleq{} |f[x]|
26. |(g[x] - g[y]) * f[x]| \mleq{} ((r1/r((2 * n) * N)) * |f[x]|)
\mvdash{} (|f[x] * (g[x] - g[y])| + |(f[x] - f[y]) * g[y]|) \mleq{} (r1/r(n))
By
Latex:
Assert \mkleeneopen{}(|f[x]| \mleq{} r(N)) \mwedge{} (|g[y]| \mleq{} r(N))\mkleeneclose{}\mcdot{}
Home
Index