---

Step * of Lemma Riemann-sum-constant

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[c:ℝ]. ∀[k:ℕ+].  (Riemann-sum(λx.c;a;b;k) = (c * (b - a)))
BY
{ (Auto THEN DVar `b'⋅ THEN (Unhide THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. c : ℝ
5. k : ℕ+
⊢ Riemann-sum(λx.c;a;b;k) = (c * (b - a))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  DVar  `b'\mcdot{}  THEN  (Unhide  THENA  Auto))

---

Home Index