Step
*
2
1
1
1
1
of Lemma
fun-converges-to-integral
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (f[n;x] = f[n;y]))
5. a : {a:ℝ| a ∈ I}
6. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (F[x] = F[y]))
7. m : {m:ℕ+| icompact(i-approx(I;m))}
8. k : ℕ+
9. m2 : ℕ+
10. i-approx(I;m) ⊆ i-approx(I;m2)
11. a ∈ i-approx(I;m2)
12. icompact(i-approx(I;m2))
13. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . ∀n:{N...}. (|f[n;x] - F[x]| ≤ (r1/r(k)))
14. n : ℕ
15. r(-n) ≤ |i-approx(I;m2)|
16. |i-approx(I;m2)| ≤ r(n)
17. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . ∀n@0:{N...}. (|f[n@0;x] - F[x]| ≤ (r1/r((n + 1) * k)))
18. i-approx(I;m2) ⊆ I
19. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . [rmin(a;x), rmax(a;x)] ⊆ I
⊢ ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}. (|a_∫-x f[n;t] dt - a_∫-x F[t] dt| ≤ (r1/r(k)))
BY
{ Assert ⌜∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (F[x] = F[y]))⌝⋅ }
1
.....assertion.....
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (f[n;x] = f[n;y]))
5. a : {a:ℝ| a ∈ I}
6. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (F[x] = F[y]))
7. m : {m:ℕ+| icompact(i-approx(I;m))}
8. k : ℕ+
9. m2 : ℕ+
10. i-approx(I;m) ⊆ i-approx(I;m2)
11. a ∈ i-approx(I;m2)
12. icompact(i-approx(I;m2))
13. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . ∀n:{N...}. (|f[n;x] - F[x]| ≤ (r1/r(k)))
14. n : ℕ
15. r(-n) ≤ |i-approx(I;m2)|
16. |i-approx(I;m2)| ≤ r(n)
17. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . ∀n@0:{N...}. (|f[n@0;x] - F[x]| ≤ (r1/r((n + 1) * k)))
18. i-approx(I;m2) ⊆ I
19. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . [rmin(a;x), rmax(a;x)] ⊆ I
⊢ ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (F[x] = F[y]))
2
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (f[n;x] = f[n;y]))
5. a : {a:ℝ| a ∈ I}
6. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (F[x] = F[y]))
7. m : {m:ℕ+| icompact(i-approx(I;m))}
8. k : ℕ+
9. m2 : ℕ+
10. i-approx(I;m) ⊆ i-approx(I;m2)
11. a ∈ i-approx(I;m2)
12. icompact(i-approx(I;m2))
13. ∀k:ℕ+. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . ∀n:{N...}. (|f[n;x] - F[x]| ≤ (r1/r(k)))
14. n : ℕ
15. r(-n) ≤ |i-approx(I;m2)|
16. |i-approx(I;m2)| ≤ r(n)
17. ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . ∀n@0:{N...}. (|f[n@0;x] - F[x]| ≤ (r1/r((n + 1) * k)))
18. i-approx(I;m2) ⊆ I
19. ∀x:{x:ℝ| x ∈ i-approx(I;m2)} . [rmin(a;x), rmax(a;x)] ⊆ I
20. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (F[x] = F[y]))
⊢ ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}. (|a_∫-x f[n;t] dt - a_∫-x F[t] dt| ≤ (r1/r(k)))
Latex:
Latex:
1. I : Interval
2. f : \mBbbN{} {}\mrightarrow{} I {}\mrightarrow{}\mBbbR{}
3. F : I {}\mrightarrow{}\mBbbR{}
4. \mforall{}n:\mBbbN{}. \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} (f[n;x] = f[n;y]))
5. a : \{a:\mBbbR{}| a \mmember{} I\}
6. \mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} (F[x] = F[y]))
7. m : \{m:\mBbbN{}\msupplus{}| icompact(i-approx(I;m))\}
8. k : \mBbbN{}\msupplus{}
9. m2 : \mBbbN{}\msupplus{}
10. i-approx(I;m) \msubseteq{} i-approx(I;m2)
11. a \mmember{} i-approx(I;m2)
12. icompact(i-approx(I;m2))
13. \mforall{}k:\mBbbN{}\msupplus{}. \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;m2)\} . \mforall{}n:\{N...\}. (|f[n;x] - F[x]| \mleq{} (r1/r(k)))
14. n : \mBbbN{}
15. r(-n) \mleq{} |i-approx(I;m2)|
16. |i-approx(I;m2)| \mleq{} r(n)
17. \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;m2)\} . \mforall{}n@0:\{N...\}. (|f[n@0;x] - F[x]| \mleq{} (r1/r((n + 1) * k)))
18. i-approx(I;m2) \msubseteq{} I
19. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;m2)\} . [rmin(a;x), rmax(a;x)] \msubseteq{} I
\mvdash{} \mexists{}N:\mBbbN{}\msupplus{}. \mforall{}x:\{x:\mBbbR{}| x \mmember{} i-approx(I;m)\} . \mforall{}n:\{N...\}. (|a\_\mint{}\msupminus{}x f[n;t] dt - a\_\mint{}\msupminus{}x F[t] dt| \mleq{} (r1/r(k)))
By
Latex:
Assert \mkleeneopen{}\mforall{}x,y:\{t:\mBbbR{}| t \mmember{} I\} . ((x = y) {}\mRightarrow{} (F[x] = F[y]))\mkleeneclose{}\mcdot{}
Home
Index