Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.integral_deriv_eq_sub

∀ {f : ℝ → ℝ} {a b : ℝ}, AbsolutelyContinuousOnInterval f a b → ∫ (x : ℝ) in a..b, deriv f x = f b - f a

Fundamental Theorem of Calculus for absolutely continuous functions: if f is absolutely continuous on uIcc a b, then ∫ (x : ℝ) in a..b, deriv f x = f b - f a.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Cited by

1 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound