---

Step * 2 1 of Lemma fun-converges-to-integral


1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. ∀m:{m:ℕ+| icompact(i-approx(I;m))} . ∀k:ℕ+.
     ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - F[x]| ≤ (r1/r(k)))
5. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[n;x] = f[n;y]))
6. a : {a:ℝ| a ∈ I} 
7. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (F[x] = F[y]))
8. m : {m:ℕ+| icompact(i-approx(I;m))} 
9. k : ℕ+
⊢ ∃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 ∃m2:ℕ+. (i-approx(I;m) ⊆ i-approx(I;m2)  ∧ (a ∈ i-approx(I;m2))) BY
         ((InstLemma `i-approx-containing2` [⌜I⌝;⌜a⌝;⌜a⌝]⋅ THENA Auto)
          THEN ExRepD
          THEN D 0 With ⌜imax(n;m)⌝ 
          THEN Auto
          THEN (InstLemma `i-approx-monotonic` [⌜I⌝;⌜m⌝;⌜imax(n;m)⌝]⋅ THEN Auto)
          THEN InstLemma `i-approx-monotonic` [⌜I⌝;⌜n⌝;⌜imax(n;m)⌝]⋅
          THEN Auto)) }

1
1. I : Interval
2. f : ℕ ⟶ I ⟶ℝ
3. F : I ⟶ℝ
4. ∀m:{m:ℕ+| icompact(i-approx(I;m))} . ∀k:ℕ+.
     ∃N:ℕ+. ∀x:{x:ℝ| x ∈ i-approx(I;m)} . ∀n:{N...}.  (|f[n;x] - F[x]| ≤ (r1/r(k)))
5. ∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (f[n;x] = f[n;y]))
6. a : {a:ℝ| a ∈ I} 
7. ∀x,y:{t:ℝ| t ∈ I} .  ((x = y) ⇒ (F[x] = F[y]))
8. m : {m:ℕ+| icompact(i-approx(I;m))} 
9. k : ℕ+
10. ∃m2:ℕ+. (i-approx(I;m) ⊆ i-approx(I;m2)  ∧ (a ∈ i-approx(I;m2)))
⊢ ∃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{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\}  .  \mforall{}k:\mBbbN{}\msupplus{}.
          \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\}  .  \mforall{}n:\{N...\}.    (|f[n;x]  -  F[x]|  \mleq{}  (r1/r(k)))
5.  \mforall{}n:\mBbbN{}.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f[n;x]  =  f[n;y]))
6.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
7.  \mforall{}x,y:\{t:\mBbbR{}|  t  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (F[x]  =  F[y]))
8.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
9.  k  :  \mBbbN{}\msupplus{}
\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  \mexists{}m2:\mBbbN{}\msupplus{}.  (i-approx(I;m)  \msubseteq{}  i-approx(I;m2)    \mwedge{}  (a  \mmember{}  i-approx(I;m2)))  BY
              ((InstLemma  `i-approx-containing2`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD
                THEN  D  0  With  \mkleeneopen{}imax(n;m)\mkleeneclose{} 
                THEN  Auto
                THEN  (InstLemma  `i-approx-monotonic`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}imax(n;m)\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  InstLemma  `i-approx-monotonic`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}imax(n;m)\mkleeneclose{}]\mcdot{}
                THEN  Auto))

---

Home Index