Step
*
1
1
2
1
3
4
1
1
1
1
1
1
1
2
1
1
1
1
1
1
1
1
1
1
2
1
2
of Lemma
partition-refinement-sum
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. ∀m,n:ℕ+.
(mc m n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))} )
6. K : ℕ
7. ∀K:ℕK. ∀J:Interval.
(icompact(J)
⇒ J ⊆ I
⇒ (∀q:partition(J)
((||q|| ≤ K)
⇒ (∀n:ℕ+
((partition-mesh(J;q) ≤ (mc 1 n))
⇒ frs-increasing(q)
⇒ (∀p:partition(J). ∀x:partition-choice(full-partition(J;p)).
∀y:partition-choice(full-partition(J;q)).
(p refines q
⇒ (|S(f;full-partition(J;q)) - S(f;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)))))))))
8. J : Interval
9. icompact(J)
10. J ⊆ I
11. u : ℝ
12. v : ℝ List
13. partitions(J;[u / v])
14. ||[u / v]|| ≤ K
15. n : ℕ+
16. partition-mesh(J;[u / v]) ≤ (mc 1 n)
17. frs-increasing([u / v])
18. p : partition(J)
19. x : partition-choice(full-partition(J;p))
20. y : partition-choice(full-partition(J;[u / v]))
21. p refines [u / v]
22. partitions([left-endpoint(J), u];[])
23. partitions([u, right-endpoint(J)];v)
24. left-endpoint(J) ≤ u
25. u ≤ right-endpoint(J)
26. partition-mesh([left-endpoint(J), u];[]) ≤ partition-mesh(J;[u / v])
27. partition-mesh([u, right-endpoint(J)];v) ≤ partition-mesh(J;[u / v])
28. u ∈ J
29. left-endpoint(J) ∈ J
30. right-endpoint(J) ∈ J
31. q : partition([left-endpoint(J), u])
32. r : partition([u, right-endpoint(J)])
33. q refines []
34. r refines v
35. x1 : ℝ
36. x1 = u
37. p = (q @ [x1 / r]) ∈ (ℝ List)
38. ||r|| + ||q|| < ||p||
39. is-partition-choice(full-partition([left-endpoint(J), u];q);x)
∧ is-partition-choice(full-partition([u, right-endpoint(J)];r);λi.(x (i + ||q|| + 1)))
40. icompact([left-endpoint(J), u]) ∧ icompact([u, right-endpoint(J)])
41. (||r|| + ||q|| + 1) + 1 < ||full-partition(J;p)||
42. λi.(x (i + ||q|| + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];r))
43. x ∈ partition-choice(full-partition([left-endpoint(J), u];q))
44. ||v|| + 2 < ||full-partition(J;[u / v])||
45. λi.(y 0) ∈ partition-choice(full-partition([left-endpoint(J), u];[]))
46. |S(f;full-partition([left-endpoint(J), u];[])) - S(f;full-partition([left-endpoint(J), u];q))| ≤ ((r1/r(n))
* |[left-endpoint(J), u]|)
47. λi.(y (i + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];v))
48. |S(f;full-partition([u, right-endpoint(J)];v)) - S(f;full-partition([u, right-endpoint(J)];r))| ≤ ((r1/r(n))
* |[u, right-endpoint(J)]|)
49. v1 : ℝ
50. left-endpoint(J) = v1 ∈ ℝ
51. v2 : ℝ
52. right-endpoint(J) = v2 ∈ ℝ
53. v3 : ℝ List
54. [u / (v @ [v2])] = v3 ∈ (ℝ List)
55. ||v3|| = (||v|| + 2) ∈ ℤ
56. ∀[x:ℕ(((||v|| + 2) + 1) - 2) + 1 ⟶ ℝ]
(Σ{x[i] | 0≤i≤((||v|| + 2) + 1) - 2}
= (Σ{x[i] | 0≤i≤0} + Σ{x[0 + i + 1] | 0≤i≤((||v|| + 2) + 1) - 2 - 0 + 1})) supposing
((0 ≤ (((||v|| + 2) + 1) - 2)) and
(0 ≤ 0))
57. i : ℕ||v|| + 2
58. ∀i:ℕ||full-partition(J;[u / v])|| - 1. (y i ∈ {x:ℝ| x ∈ J} )
59. y i ∈ {x:ℝ| x ∈ J}
⊢ y i ∈ {x:ℝ| x ∈ I}
BY
{ DoSubsume⋅ }
1
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. ∀m,n:ℕ+.
(mc m n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))} )
6. K : ℕ
7. ∀K:ℕK. ∀J:Interval.
(icompact(J)
⇒ J ⊆ I
⇒ (∀q:partition(J)
((||q|| ≤ K)
⇒ (∀n:ℕ+
((partition-mesh(J;q) ≤ (mc 1 n))
⇒ frs-increasing(q)
⇒ (∀p:partition(J). ∀x:partition-choice(full-partition(J;p)).
∀y:partition-choice(full-partition(J;q)).
(p refines q
⇒ (|S(f;full-partition(J;q)) - S(f;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)))))))))
8. J : Interval
9. icompact(J)
10. J ⊆ I
11. u : ℝ
12. v : ℝ List
13. partitions(J;[u / v])
14. ||[u / v]|| ≤ K
15. n : ℕ+
16. partition-mesh(J;[u / v]) ≤ (mc 1 n)
17. frs-increasing([u / v])
18. p : partition(J)
19. x : partition-choice(full-partition(J;p))
20. y : partition-choice(full-partition(J;[u / v]))
21. p refines [u / v]
22. partitions([left-endpoint(J), u];[])
23. partitions([u, right-endpoint(J)];v)
24. left-endpoint(J) ≤ u
25. u ≤ right-endpoint(J)
26. partition-mesh([left-endpoint(J), u];[]) ≤ partition-mesh(J;[u / v])
27. partition-mesh([u, right-endpoint(J)];v) ≤ partition-mesh(J;[u / v])
28. u ∈ J
29. left-endpoint(J) ∈ J
30. right-endpoint(J) ∈ J
31. q : partition([left-endpoint(J), u])
32. r : partition([u, right-endpoint(J)])
33. q refines []
34. r refines v
35. x1 : ℝ
36. x1 = u
37. p = (q @ [x1 / r]) ∈ (ℝ List)
38. ||r|| + ||q|| < ||p||
39. is-partition-choice(full-partition([left-endpoint(J), u];q);x)
∧ is-partition-choice(full-partition([u, right-endpoint(J)];r);λi.(x (i + ||q|| + 1)))
40. icompact([left-endpoint(J), u]) ∧ icompact([u, right-endpoint(J)])
41. (||r|| + ||q|| + 1) + 1 < ||full-partition(J;p)||
42. λi.(x (i + ||q|| + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];r))
43. x ∈ partition-choice(full-partition([left-endpoint(J), u];q))
44. ||v|| + 2 < ||full-partition(J;[u / v])||
45. λi.(y 0) ∈ partition-choice(full-partition([left-endpoint(J), u];[]))
46. |S(f;full-partition([left-endpoint(J), u];[])) - S(f;full-partition([left-endpoint(J), u];q))| ≤ ((r1/r(n))
* |[left-endpoint(J), u]|)
47. λi.(y (i + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];v))
48. |S(f;full-partition([u, right-endpoint(J)];v)) - S(f;full-partition([u, right-endpoint(J)];r))| ≤ ((r1/r(n))
* |[u, right-endpoint(J)]|)
49. v1 : ℝ
50. left-endpoint(J) = v1 ∈ ℝ
51. v2 : ℝ
52. right-endpoint(J) = v2 ∈ ℝ
53. v3 : ℝ List
54. [u / (v @ [v2])] = v3 ∈ (ℝ List)
55. ||v3|| = (||v|| + 2) ∈ ℤ
56. ∀[x:ℕ(((||v|| + 2) + 1) - 2) + 1 ⟶ ℝ]
(Σ{x[i] | 0≤i≤((||v|| + 2) + 1) - 2}
= (Σ{x[i] | 0≤i≤0} + Σ{x[0 + i + 1] | 0≤i≤((||v|| + 2) + 1) - 2 - 0 + 1})) supposing
((0 ≤ (((||v|| + 2) + 1) - 2)) and
(0 ≤ 0))
57. i : ℕ||v|| + 2
58. ∀i:ℕ||full-partition(J;[u / v])|| - 1. (y i ∈ {x:ℝ| x ∈ J} )
59. y i ∈ {x:ℝ| x ∈ J}
⊢ y i ∈ {x:ℝ| x ∈ J}
2
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. ∀m,n:ℕ+.
(mc m n ∈ {d:ℝ| (r0 < d) ∧ (∀x,y:ℝ. ((x ∈ I) ⇒ (y ∈ I) ⇒ (|x - y| ≤ d) ⇒ (|f[x] - f[y]| ≤ (r1/r(n)))))} )
6. K : ℕ
7. ∀K:ℕK. ∀J:Interval.
(icompact(J)
⇒ J ⊆ I
⇒ (∀q:partition(J)
((||q|| ≤ K)
⇒ (∀n:ℕ+
((partition-mesh(J;q) ≤ (mc 1 n))
⇒ frs-increasing(q)
⇒ (∀p:partition(J). ∀x:partition-choice(full-partition(J;p)).
∀y:partition-choice(full-partition(J;q)).
(p refines q
⇒ (|S(f;full-partition(J;q)) - S(f;full-partition(J;p))| ≤ ((r1/r(n)) * |J|)))))))))
8. J : Interval
9. icompact(J)
10. J ⊆ I
11. u : ℝ
12. v : ℝ List
13. partitions(J;[u / v])
14. ||[u / v]|| ≤ K
15. n : ℕ+
16. partition-mesh(J;[u / v]) ≤ (mc 1 n)
17. frs-increasing([u / v])
18. p : partition(J)
19. x : partition-choice(full-partition(J;p))
20. y : partition-choice(full-partition(J;[u / v]))
21. p refines [u / v]
22. partitions([left-endpoint(J), u];[])
23. partitions([u, right-endpoint(J)];v)
24. left-endpoint(J) ≤ u
25. u ≤ right-endpoint(J)
26. partition-mesh([left-endpoint(J), u];[]) ≤ partition-mesh(J;[u / v])
27. partition-mesh([u, right-endpoint(J)];v) ≤ partition-mesh(J;[u / v])
28. u ∈ J
29. left-endpoint(J) ∈ J
30. right-endpoint(J) ∈ J
31. q : partition([left-endpoint(J), u])
32. r : partition([u, right-endpoint(J)])
33. q refines []
34. r refines v
35. x1 : ℝ
36. x1 = u
37. p = (q @ [x1 / r]) ∈ (ℝ List)
38. ||r|| + ||q|| < ||p||
39. is-partition-choice(full-partition([left-endpoint(J), u];q);x)
∧ is-partition-choice(full-partition([u, right-endpoint(J)];r);λi.(x (i + ||q|| + 1)))
40. icompact([left-endpoint(J), u]) ∧ icompact([u, right-endpoint(J)])
41. (||r|| + ||q|| + 1) + 1 < ||full-partition(J;p)||
42. λi.(x (i + ||q|| + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];r))
43. x ∈ partition-choice(full-partition([left-endpoint(J), u];q))
44. ||v|| + 2 < ||full-partition(J;[u / v])||
45. λi.(y 0) ∈ partition-choice(full-partition([left-endpoint(J), u];[]))
46. |S(f;full-partition([left-endpoint(J), u];[])) - S(f;full-partition([left-endpoint(J), u];q))| ≤ ((r1/r(n))
* |[left-endpoint(J), u]|)
47. λi.(y (i + 1)) ∈ partition-choice(full-partition([u, right-endpoint(J)];v))
48. |S(f;full-partition([u, right-endpoint(J)];v)) - S(f;full-partition([u, right-endpoint(J)];r))| ≤ ((r1/r(n))
* |[u, right-endpoint(J)]|)
49. v1 : ℝ
50. left-endpoint(J) = v1 ∈ ℝ
51. v2 : ℝ
52. right-endpoint(J) = v2 ∈ ℝ
53. v3 : ℝ List
54. [u / (v @ [v2])] = v3 ∈ (ℝ List)
55. ||v3|| = (||v|| + 2) ∈ ℤ
56. ∀[x:ℕ(((||v|| + 2) + 1) - 2) + 1 ⟶ ℝ]
(Σ{x[i] | 0≤i≤((||v|| + 2) + 1) - 2}
= (Σ{x[i] | 0≤i≤0} + Σ{x[0 + i + 1] | 0≤i≤((||v|| + 2) + 1) - 2 - 0 + 1})) supposing
((0 ≤ (((||v|| + 2) + 1) - 2)) and
(0 ≤ 0))
57. i : ℕ||v|| + 2
58. ∀i:ℕ||full-partition(J;[u / v])|| - 1. (y i ∈ {x:ℝ| x ∈ J} )
59. y i ∈ {x:ℝ| x ∈ J}
60. (y i) = (y i) ∈ {x:ℝ| x ∈ J}
⊢ {x:ℝ| x ∈ J} ⊆r {x:ℝ| x ∈ I}
Latex:
Latex:
1. I : Interval
2. icompact(I)
3. f : I {}\mrightarrow{}\mBbbR{}
4. mc : f[x] continuous for x \mmember{} I
5. \mforall{}m,n:\mBbbN{}\msupplus{}.
(mc m n \mmember{} \{d:\mBbbR{}|
(r0 < d)
\mwedge{} (\mforall{}x,y:\mBbbR{}. ((x \mmember{} I) {}\mRightarrow{} (y \mmember{} I) {}\mRightarrow{} (|x - y| \mleq{} d) {}\mRightarrow{} (|f[x] - f[y]| \mleq{} (r1/r(n)))))\} )
6. K : \mBbbN{}
7. \mforall{}K:\mBbbN{}K. \mforall{}J:Interval.
(icompact(J)
{}\mRightarrow{} J \msubseteq{} I
{}\mRightarrow{} (\mforall{}q:partition(J)
((||q|| \mleq{} K)
{}\mRightarrow{} (\mforall{}n:\mBbbN{}\msupplus{}
((partition-mesh(J;q) \mleq{} (mc 1 n))
{}\mRightarrow{} frs-increasing(q)
{}\mRightarrow{} (\mforall{}p:partition(J). \mforall{}x:partition-choice(full-partition(J;p)).
\mforall{}y:partition-choice(full-partition(J;q)).
(p refines q
{}\mRightarrow{} (|S(f;full-partition(J;q)) - S(f;full-partition(J;p))| \mleq{} ((r1/r(n))
* |J|)))))))))
8. J : Interval
9. icompact(J)
10. J \msubseteq{} I
11. u : \mBbbR{}
12. v : \mBbbR{} List
13. partitions(J;[u / v])
14. ||[u / v]|| \mleq{} K
15. n : \mBbbN{}\msupplus{}
16. partition-mesh(J;[u / v]) \mleq{} (mc 1 n)
17. frs-increasing([u / v])
18. p : partition(J)
19. x : partition-choice(full-partition(J;p))
20. y : partition-choice(full-partition(J;[u / v]))
21. p refines [u / v]
22. partitions([left-endpoint(J), u];[])
23. partitions([u, right-endpoint(J)];v)
24. left-endpoint(J) \mleq{} u
25. u \mleq{} right-endpoint(J)
26. partition-mesh([left-endpoint(J), u];[]) \mleq{} partition-mesh(J;[u / v])
27. partition-mesh([u, right-endpoint(J)];v) \mleq{} partition-mesh(J;[u / v])
28. u \mmember{} J
29. left-endpoint(J) \mmember{} J
30. right-endpoint(J) \mmember{} J
31. q : partition([left-endpoint(J), u])
32. r : partition([u, right-endpoint(J)])
33. q refines []
34. r refines v
35. x1 : \mBbbR{}
36. x1 = u
37. p = (q @ [x1 / r])
38. ||r|| + ||q|| < ||p||
39. is-partition-choice(full-partition([left-endpoint(J), u];q);x)
\mwedge{} is-partition-choice(full-partition([u, right-endpoint(J)];r);\mlambda{}i.(x (i + ||q|| + 1)))
40. icompact([left-endpoint(J), u]) \mwedge{} icompact([u, right-endpoint(J)])
41. (||r|| + ||q|| + 1) + 1 < ||full-partition(J;p)||
42. \mlambda{}i.(x (i + ||q|| + 1)) \mmember{} partition-choice(full-partition([u, right-endpoint(J)];r))
43. x \mmember{} partition-choice(full-partition([left-endpoint(J), u];q))
44. ||v|| + 2 < ||full-partition(J;[u / v])||
45. \mlambda{}i.(y 0) \mmember{} partition-choice(full-partition([left-endpoint(J), u];[]))
46. |S(f;full-partition([left-endpoint(J), u];[]))
- S(f;full-partition([left-endpoint(J), u];q))| \mleq{} ((r1/r(n)) * |[left-endpoint(J), u]|)
47. \mlambda{}i.(y (i + 1)) \mmember{} partition-choice(full-partition([u, right-endpoint(J)];v))
48. |S(f;full-partition([u, right-endpoint(J)];v))
- S(f;full-partition([u, right-endpoint(J)];r))| \mleq{} ((r1/r(n)) * |[u, right-endpoint(J)]|)
49. v1 : \mBbbR{}
50. left-endpoint(J) = v1
51. v2 : \mBbbR{}
52. right-endpoint(J) = v2
53. v3 : \mBbbR{} List
54. [u / (v @ [v2])] = v3
55. ||v3|| = (||v|| + 2)
56. \mforall{}[x:\mBbbN{}(((||v|| + 2) + 1) - 2) + 1 {}\mrightarrow{} \mBbbR{}]
(\mSigma{}\{x[i] | 0\mleq{}i\mleq{}((||v|| + 2) + 1) - 2\}
= (\mSigma{}\{x[i] | 0\mleq{}i\mleq{}0\} + \mSigma{}\{x[0 + i + 1] | 0\mleq{}i\mleq{}((||v|| + 2) + 1) - 2 - 0 + 1\})) supposing
((0 \mleq{} (((||v|| + 2) + 1) - 2)) and
(0 \mleq{} 0))
57. i : \mBbbN{}||v|| + 2
58. \mforall{}i:\mBbbN{}||full-partition(J;[u / v])|| - 1. (y i \mmember{} \{x:\mBbbR{}| x \mmember{} J\} )
59. y i \mmember{} \{x:\mBbbR{}| x \mmember{} J\}
\mvdash{} y i \mmember{} \{x:\mBbbR{}| x \mmember{} I\}
By
Latex:
DoSubsume\mcdot{}
Home
Index