---

Step * of Lemma Riemann-sum-rmul-constant

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

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

---

Latex:

---

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


By

---

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

---

Home Index