Step
*
1
1
2
2
of Lemma
nearby-separated-partition-sum
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. f : I ⟶ℝ@i
5. mc : f[x] continuous for x ∈ I@i
6. alpha : {alpha:ℝ| r0 < alpha} @i
7. e : {e:ℝ| r0 < e} @i
8. p : partition(I)@i
9. q : partition(I)@i
10. x : partition-choice(full-partition(I;p))@i
11. y : partition-choice(full-partition(I;q))@i
12. r0 < (alpha/r(2))
13. r0 < (e/r(2))
14. e1 : {e:ℝ| r0 < e}
15. ∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
(nearby-partitions(e1;p;q)
⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e1))
⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (alpha/r(2))))
16. e2 : {e:ℝ| r0 < e}
17. ∀q@0:partition(I). ∀y@0:partition-choice(full-partition(I;q@0)).
(nearby-partitions(e2;q;q@0)
⇒ (∀i:ℕ||q|| + 1. (|y[i] - y@0[i]| ≤ e2))
⇒ (|S(f;full-partition(I;q@0)) - S(f;full-partition(I;q))| ≤ (alpha/r(2))))
18. r0 < rmin((e/r(2));rmin(e1;e2))
19. p' : partition(I)
20. ∃q':partition(I)
(separated-partitions(p';q')
∧ nearby-partitions(rmin((e/r(2));rmin(e1;e2));p;p')
∧ nearby-partitions(rmin((e/r(2));rmin(e1;e2));q;q'))
21. nearby-partitions(e1;p;p')
22. y1 : partition-choice(full-partition(I;p'))
23. ∀i:ℕ||p|| + 1. (|x[i] - y1[i]| ≤ e1)
24. partition-mesh(I;p') ≤ (partition-mesh(I;p) + e)
⊢ ∃q':partition(I)
∃y':partition-choice(full-partition(I;q'))
(separated-partitions(p';q')
∧ (partition-mesh(I;q') ≤ (partition-mesh(I;q) + e))
∧ (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| ≤ (|S(f;full-partition(I;p')) - S(f;full-partition(I;q'))|
+ alpha)))
BY
{ (ParallelOp -5 THEN (InstLemma `nearby-partition-choice` [⌜I⌝;⌜q⌝;⌜q'⌝;⌜e2⌝;⌜y⌝]⋅ THENA Auto)) }
1
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. f : I ⟶ℝ@i
5. mc : f[x] continuous for x ∈ I@i
6. alpha : {alpha:ℝ| r0 < alpha} @i
7. e : {e:ℝ| r0 < e} @i
8. p : partition(I)@i
9. q : partition(I)@i
10. x : partition-choice(full-partition(I;p))@i
11. y : partition-choice(full-partition(I;q))@i
12. r0 < (alpha/r(2))
13. r0 < (e/r(2))
14. e1 : {e:ℝ| r0 < e}
15. ∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
(nearby-partitions(e1;p;q)
⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e1))
⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (alpha/r(2))))
16. e2 : {e:ℝ| r0 < e}
17. ∀q@0:partition(I). ∀y@0:partition-choice(full-partition(I;q@0)).
(nearby-partitions(e2;q;q@0)
⇒ (∀i:ℕ||q|| + 1. (|y[i] - y@0[i]| ≤ e2))
⇒ (|S(f;full-partition(I;q@0)) - S(f;full-partition(I;q))| ≤ (alpha/r(2))))
18. r0 < rmin((e/r(2));rmin(e1;e2))
19. p' : partition(I)
20. q' : partition(I)
21. separated-partitions(p';q')
22. nearby-partitions(rmin((e/r(2));rmin(e1;e2));p;p')
23. nearby-partitions(rmin((e/r(2));rmin(e1;e2));q;q')
24. nearby-partitions(e1;p;p')
25. y1 : partition-choice(full-partition(I;p'))
26. ∀i:ℕ||p|| + 1. (|x[i] - y1[i]| ≤ e1)
27. partition-mesh(I;p') ≤ (partition-mesh(I;p) + e)
⊢ nearby-partitions(e2;q;q')
2
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. f : I ⟶ℝ@i
5. mc : f[x] continuous for x ∈ I@i
6. alpha : {alpha:ℝ| r0 < alpha} @i
7. e : {e:ℝ| r0 < e} @i
8. p : partition(I)@i
9. q : partition(I)@i
10. x : partition-choice(full-partition(I;p))@i
11. y : partition-choice(full-partition(I;q))@i
12. r0 < (alpha/r(2))
13. r0 < (e/r(2))
14. e1 : {e:ℝ| r0 < e}
15. ∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
(nearby-partitions(e1;p;q)
⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e1))
⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (alpha/r(2))))
16. e2 : {e:ℝ| r0 < e}
17. ∀q@0:partition(I). ∀y@0:partition-choice(full-partition(I;q@0)).
(nearby-partitions(e2;q;q@0)
⇒ (∀i:ℕ||q|| + 1. (|y[i] - y@0[i]| ≤ e2))
⇒ (|S(f;full-partition(I;q@0)) - S(f;full-partition(I;q))| ≤ (alpha/r(2))))
18. r0 < rmin((e/r(2));rmin(e1;e2))
19. p' : partition(I)
20. q' : partition(I)
21. separated-partitions(p';q')
∧ nearby-partitions(rmin((e/r(2));rmin(e1;e2));p;p')
∧ nearby-partitions(rmin((e/r(2));rmin(e1;e2));q;q')
22. nearby-partitions(e1;p;p')
23. y1 : partition-choice(full-partition(I;p'))
24. ∀i:ℕ||p|| + 1. (|x[i] - y1[i]| ≤ e1)
25. partition-mesh(I;p') ≤ (partition-mesh(I;p) + e)
26. ∃y@0:partition-choice(full-partition(I;q')). ∀i:ℕ||q|| + 1. (|y[i] - y@0[i]| ≤ e2)
⊢ ∃y':partition-choice(full-partition(I;q'))
(separated-partitions(p';q')
∧ (partition-mesh(I;q') ≤ (partition-mesh(I;q) + e))
∧ (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| ≤ (|S(f;full-partition(I;p')) - S(f;full-partition(I;q'))|
+ alpha)))
Latex:
Latex:
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. f : I {}\mrightarrow{}\mBbbR{}@i
5. mc : f[x] continuous for x \mmember{} I@i
6. alpha : \{alpha:\mBbbR{}| r0 < alpha\} @i
7. e : \{e:\mBbbR{}| r0 < e\} @i
8. p : partition(I)@i
9. q : partition(I)@i
10. x : partition-choice(full-partition(I;p))@i
11. y : partition-choice(full-partition(I;q))@i
12. r0 < (alpha/r(2))
13. r0 < (e/r(2))
14. e1 : \{e:\mBbbR{}| r0 < e\}
15. \mforall{}q:partition(I). \mforall{}y:partition-choice(full-partition(I;q)).
(nearby-partitions(e1;p;q)
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||p|| + 1. (|x[i] - y[i]| \mleq{} e1))
{}\mRightarrow{} (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| \mleq{} (alpha/r(2))))
16. e2 : \{e:\mBbbR{}| r0 < e\}
17. \mforall{}q@0:partition(I). \mforall{}y@0:partition-choice(full-partition(I;q@0)).
(nearby-partitions(e2;q;q@0)
{}\mRightarrow{} (\mforall{}i:\mBbbN{}||q|| + 1. (|y[i] - y@0[i]| \mleq{} e2))
{}\mRightarrow{} (|S(f;full-partition(I;q@0)) - S(f;full-partition(I;q))| \mleq{} (alpha/r(2))))
18. r0 < rmin((e/r(2));rmin(e1;e2))
19. p' : partition(I)
20. \mexists{}q':partition(I)
(separated-partitions(p';q')
\mwedge{} nearby-partitions(rmin((e/r(2));rmin(e1;e2));p;p')
\mwedge{} nearby-partitions(rmin((e/r(2));rmin(e1;e2));q;q'))
21. nearby-partitions(e1;p;p')
22. y1 : partition-choice(full-partition(I;p'))
23. \mforall{}i:\mBbbN{}||p|| + 1. (|x[i] - y1[i]| \mleq{} e1)
24. partition-mesh(I;p') \mleq{} (partition-mesh(I;p) + e)
\mvdash{} \mexists{}q':partition(I)
\mexists{}y':partition-choice(full-partition(I;q'))
(separated-partitions(p';q')
\mwedge{} (partition-mesh(I;q') \mleq{} (partition-mesh(I;q) + e))
\mwedge{} (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| \mleq{} (|S(f;full-partition(I;p'))
- S(f;full-partition(I;q'))|
+ alpha)))
By
Latex:
(ParallelOp -5 THEN (InstLemma `nearby-partition-choice` [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}q'\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{} THENA Auto))
Home
Index