---

Step * of Lemma partition-sums-converge

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} . ∀e:{e:ℝ| r0 < e} .
  ∃d:{d:ℝ| r0 < d} 
   ∀p:partition([a, b])
     ((partition-mesh([a, b];p) ≤ d)
     ⇒ (∀y:partition-choice(full-partition([a, b];p))
           (|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ e)))
BY
{ TACTIC:(Auto
          THEN All (Unfold `so_apply`)
          THEN (Assert icompact([a, b]) BY
                      EAuto 1)
          THEN (InstLemma `general-partition-sum-no-mc` [⌜[a, b]⌝;⌜λx.(f x)⌝;⌜e⌝]⋅ THENA Auto)
          THEN ParallelLast
          THEN Auto
          THEN (InstLemma `Riemann-sums-converge-to` [⌜a⌝;⌜b⌝;⌜f⌝]⋅ THENA Auto)) }

1
1. a : ℝ@i
2. b : {b:ℝ| a ≤ b} @i
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} @i
4. e : {e:ℝ| r0 < e} @i
5. icompact([a, b])
6. d : {d:ℝ| r0 < d} 
7. ∀p,q:{p:partition([a, b])| partition-mesh([a, b];p) ≤ d} . ∀x:partition-choice(full-partition([a, b];p)).
   ∀y:partition-choice(full-partition([a, b];q)).
     (|S(λx.(f x);full-partition([a, b];q)) - S(λx.(f x);full-partition([a, b];p))| ≤ e)
8. p : partition([a, b])@i
9. partition-mesh([a, b];p) ≤ d
10. y : partition-choice(full-partition([a, b];p))@i
11. lim k→∞.Riemann-sum(λx.f[x];a;b;k + 1) = ∫ f[x] dx on [a, b]
⊢ |S(λx.(f x);full-partition([a, b];p)) - ∫ f x dx on [a, b]| ≤ e

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:\{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\}  .  \mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .
    \mexists{}d:\{d:\mBbbR{}|  r0  <  d\} 
      \mforall{}p:partition([a,  b])
          ((partition-mesh([a,  b];p)  \mleq{}  d)
          {}\mRightarrow{}  (\mforall{}y:partition-choice(full-partition([a,  b];p))
                      (|S(\mlambda{}x.f[x];full-partition([a,  b];p))  -  \mint{}  f[x]  dx  on  [a,  b]|  \mleq{}  e)))


By

---

Latex:
TACTIC:(Auto
                THEN  All  (Unfold  `so\_apply`)
                THEN  (Assert  icompact([a,  b])  BY
                                        EAuto  1)
                THEN  (InstLemma  `general-partition-sum-no-mc`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}\mlambda{}x.(f  x)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ParallelLast
                THEN  Auto
                THEN  (InstLemma  `Riemann-sums-converge-to`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index