integral_eq_sub_of_hasDerivAt — Mathlib

English

If f is continuous on [a,b], has right derivative f'(x) on (a,b), and f' is interval-integrable on [a,b], then ∫ f' = f(b) − f(a).

Русский

Если f непрерывна на [a,b], имеет правую производную на (a,b) и f' интегрируема на [a,b], тогда ∫ f' = f(b) − f(a).

LaTeX

$$$\\int_{a}^{b} f'(y) dy = f(b)-f(a)$$$

Lean4

/-- Fundamental theorem of calculus-2: If `f : ℝ → E` has a derivative at `f' x` for all `x` in
  `[a, b]` and `f'` is integrable on `[a, b]`, then `∫ y in a..b, f' y` equals `f b - f a`. -/
theorem integral_eq_sub_of_hasDerivAt (hderiv : ∀ x ∈ uIcc a b, HasDerivAt f (f' x) x)
    (hint : IntervalIntegrable f' volume a b) : ∫ y in a..b, f' y = f b - f a :=
  integral_eq_sub_of_hasDeriv_right (HasDerivAt.continuousOn hderiv)
    (fun _x hx => (hderiv _ (mem_Icc_of_Ioo hx)).hasDerivWithinAt) hint

Похожие утверждения