---

Step * of Lemma Riemann-sums-converge-no-mc

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} .  Riemann-sum(f;a;b;k + 1)↓ as k→∞
BY
{ (EAuto 1
   THEN BLemma `converges-iff-cauchy-ext`
   THEN Auto
   THEN (D 0 THEN Auto)
   THEN RenameVar `m' (-1)
   THEN (InstLemma `general-partition-sum-no-mc` [⌜[a, b]⌝;⌜f⌝;⌜(r1/r(m))⌝]⋅ THENA (EAuto 1 THEN MemTypeCD THEN Auto))
   THEN ExRepD
   THEN (InstLemma `small-reciprocal-real` [⌜d⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstLemma `r-archimedean-implies2` [⌜|[a, b]|⌝;⌜d⌝]⋅ THENA (Auto THEN RepUR ``i-finite`` 0 THEN Auto))) }

1
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. m : ℕ+
5. d : {d:ℝ| r0 < d} 
6. ∀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(f;full-partition([a, b];q)) - S(f;full-partition([a, b];p))| ≤ (r1/r(m)))
7. k : ℕ+
8. (r1/r(k)) < d
9. ∃M:ℕ+. ((|[a, b]|/r(M)) ≤ d)
⊢ ∃N:ℕ [(∀k,m@0:ℕ.  ((N ≤ k) ⇒ (N ≤ m@0) ⇒ (|Riemann-sum(f;a;b;k + 1) - Riemann-sum(f;a;b;m@0 + 1)| ≤ (r1/r(m)))))]

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:\{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\}  .    Riemann-sum(f;a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}


By

---

Latex:
(EAuto  1
  THEN  BLemma  `converges-iff-cauchy-ext`
  THEN  Auto
  THEN  (D  0  THEN  Auto)
  THEN  RenameVar  `m'  (-1)
  THEN  (InstLemma  `general-partition-sum-no-mc`  [\mkleeneopen{}[a,  b]\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}(r1/r(m))\mkleeneclose{}]\mcdot{}
              THENA  (EAuto  1  THEN  MemTypeCD  THEN  Auto)
              )
  THEN  ExRepD
  THEN  (InstLemma  `small-reciprocal-real`  [\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstLemma  `r-archimedean-implies2`  [\mkleeneopen{}|[a,  b]|\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RepUR  ``i-finite``  0  THEN  Auto)
              ))

---

Home Index