---

Step * of Lemma rabs-Riemann-sum

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. ∀[k:ℕ+].  (|Riemann-sum(f;a;b;k)| ≤ Riemann-sum(λx.|f x|;a;b;k))
BY
{ (Auto
   THEN DVar `b'⋅
   THEN (Unhide THENA Auto)
   THEN (Assert icompact([a, b]) BY
               EAuto 1)
   THEN RepUR ``Riemann-sum let`` 0
   THEN BLemma `rabs-partition-sum`
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f:[a,  b]  {}\mrightarrow{}\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
    (|Riemann-sum(f;a;b;k)|  \mleq{}  Riemann-sum(\mlambda{}x.|f  x|;a;b;k))


By

---

Latex:
(Auto
  THEN  DVar  `b'\mcdot{}
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  icompact([a,  b])  BY
                          EAuto  1)
  THEN  RepUR  ``Riemann-sum  let``  0
  THEN  BLemma  `rabs-partition-sum`
  THEN  EAuto  1)

---

Home Index