---

Step * of Lemma Riemann-sum-rleq

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].
  Riemann-sum(f;a;b;k) ≤ Riemann-sum(g;a;b;k) supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((f x) ≤ (g x)))
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 `partition-sum-rleq`
   THEN EAuto 1) }

---

Latex:

---

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


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  `partition-sum-rleq`
  THEN  EAuto  1)

---

Home Index