Theorems · Theorem · real analysis

AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zero

∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} {a b : ℝ},
  AbsolutelyContinuousOnInterval f a b →
    (∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → HasDerivAt f 0 x) → ∃ C, ∀ x ∈ Set.uIcc a b, f x = C

If f is absolutely continuous on uIcc a b and f' x = 0 for a.e. x ∈ uIcc a b, then f is constant on uIcc a b.

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace