Zero_Derivative_implies_Constant_Function
Provedanalysiscalculusderivativesproofwiki
If f is continuous on [a,b] with zero derivative on (a,b), then f is constant on [a,b].
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue
Formal statement
import Mathlib.Analysis.Complex.Basic import Mathlib.Analysis.Calculus.MeanValue theorem Zero_Derivative_implies_Constant_Function (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : ∀ x ∈ Set.Ioo a b, HasDerivAt f 0 x) : ∀ x ∈ Set.Icc a b, f x = f a := by sorry
Source