Step
*
1
1
2
2
of Lemma
nearby-separated-partition-sum-no-mc
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. f : {f:I ⟶ℝ| ifun(f;I)} @i
5. alpha : {alpha:ℝ| r0 < alpha} @i
6. e : {e:ℝ| r0 < e} @i
7. p : partition(I)@i
8. q : partition(I)@i
9. x : partition-choice(full-partition(I;p))@i
10. y : partition-choice(full-partition(I;q))@i
11. r0 < (alpha/r(2))
12. r0 < (e/r(2))
13. e1 : {e:ℝ| r0 < e}
14. ∀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))))
15. e2 : {e:ℝ| r0 < e}
16. ∀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))))
17. r0 < rmin((e/r(2));rmin(e1;e2))
18. p' : partition(I)
19. ∃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'))
20. nearby-partitions(e1;p;p')
21. y1 : partition-choice(full-partition(I;p'))
22. ∀i:ℕ||p|| + 1. (|x[i] - y1[i]| ≤ e1)
23. 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 : {f:I ⟶ℝ| ifun(f;I)} @i
5. alpha : {alpha:ℝ| r0 < alpha} @i
6. e : {e:ℝ| r0 < e} @i
7. p : partition(I)@i
8. q : partition(I)@i
9. x : partition-choice(full-partition(I;p))@i
10. y : partition-choice(full-partition(I;q))@i
11. r0 < (alpha/r(2))
12. r0 < (e/r(2))
13. e1 : {e:ℝ| r0 < e}
14. ∀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))))
15. e2 : {e:ℝ| r0 < e}
16. ∀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))))
17. r0 < rmin((e/r(2));rmin(e1;e2))
18. p' : partition(I)
19. q' : partition(I)
20. separated-partitions(p';q')
21. nearby-partitions(rmin((e/r(2));rmin(e1;e2));p;p')
22. nearby-partitions(rmin((e/r(2));rmin(e1;e2));q;q')
23. nearby-partitions(e1;p;p')
24. y1 : partition-choice(full-partition(I;p'))
25. ∀i:ℕ||p|| + 1. (|x[i] - y1[i]| ≤ e1)
26. 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 : {f:I ⟶ℝ| ifun(f;I)} @i
5. alpha : {alpha:ℝ| r0 < alpha} @i
6. e : {e:ℝ| r0 < e} @i
7. p : partition(I)@i
8. q : partition(I)@i
9. x : partition-choice(full-partition(I;p))@i
10. y : partition-choice(full-partition(I;q))@i
11. r0 < (alpha/r(2))
12. r0 < (e/r(2))
13. e1 : {e:ℝ| r0 < e}
14. ∀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))))
15. e2 : {e:ℝ| r0 < e}
16. ∀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))))
17. r0 < rmin((e/r(2));rmin(e1;e2))
18. p' : partition(I)
19. q' : partition(I)
20. 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)
25. ∃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 : \{f:I {}\mrightarrow{}\mBbbR{}| ifun(f;I)\} @i
5. alpha : \{alpha:\mBbbR{}| r0 < alpha\} @i
6. e : \{e:\mBbbR{}| r0 < e\} @i
7. p : partition(I)@i
8. q : partition(I)@i
9. x : partition-choice(full-partition(I;p))@i
10. y : partition-choice(full-partition(I;q))@i
11. r0 < (alpha/r(2))
12. r0 < (e/r(2))
13. e1 : \{e:\mBbbR{}| r0 < e\}
14. \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))))
15. e2 : \{e:\mBbbR{}| r0 < e\}
16. \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))))
17. r0 < rmin((e/r(2));rmin(e1;e2))
18. p' : partition(I)
19. \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'))
20. nearby-partitions(e1;p;p')
21. y1 : partition-choice(full-partition(I;p'))
22. \mforall{}i:\mBbbN{}||p|| + 1. (|x[i] - y1[i]| \mleq{} e1)
23. 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