Step
*
of Lemma
Riemann-sum-radd
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].
  (Riemann-sum(λx.((f x) + (g x));a;b;k) = (Riemann-sum(f;a;b;k) + Riemann-sum(g;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. g : [a, b] ⟶ℝ
6. k : ℕ+
⊢ Riemann-sum(λx.((f x) + (g x));a;b;k) = (Riemann-sum(f;a;b;k) + Riemann-sum(g;a;b;k))
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(\mlambda{}x.((f  x)  +  (g  x));a;b;k)  =  (Riemann-sum(f;a;b;k)  +  Riemann-sum(g;a;b;k)))
By
Latex:
(Auto  THEN  DVar  `b'\mcdot{}  THEN  (Unhide  THENA  Auto))
Home
Index