English
If f is interval-integrable on [a,b] and continuous at a and b, then F(u,v) = ∫_{u}^{v} f(x) dx is differentiable with derivative given by L(h,k) = k f(b) − h f(a).
Русский
Если f интегрируема на [a,b] и непрерывна в обеих концах, то F(u,v)=∫_{u}^{v} f(x) dx дифференцируема, производная L(h,k)=k f(b) − h f(a).
LaTeX
$$$F(u,v)=\\int_{u}^{v} f(x)\\,dx,\\ dF_{(a,b)}(h,k)=k f(b) - h f(a).$$$
Lean4
/-- **Fundamental theorem of calculus-1**, strict differentiability in the right endpoint.
If `f : ℝ → E` is continuous, then `u ↦ ∫ x in a..u, f x` has derivative `f b` at `b` in the sense
of strict differentiability. -/
theorem _root_.Continuous.integral_hasStrictDerivAt {f : ℝ → E} (hf : Continuous f) (a b : ℝ) :
HasStrictDerivAt (fun u => ∫ x : ℝ in a..u, f x) (f b) b :=
integral_hasStrictDerivAt_right (hf.intervalIntegrable _ _) (hf.stronglyMeasurableAtFilter _ _) hf.continuousAt
