Theorems · Theorem · real analysis

intervalIntegral.integral_eq_sub_of_hasDeriv_right

∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} [CompleteSpace E] {f f' : ℝ → E},
  ContinuousOn f (Set.uIcc a b) →
    (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
      IntervalIntegrable f' MeasureTheory.volume a b → ∫ (y : ℝ) in a..b, f' y = f b - f a

Fundamental theorem of calculus-2: If f : ℝ → E is continuous on [a, b] and has a right 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.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus

Cited by

8 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace