Rolles_Theorem

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysiscalculusmean-value-theoremproofwiki

If f is continuous on [a,b], differentiable on (a,b), and f(a) = f(b), then there exists xi in (a,b) with f'(xi) = 0.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.MeanValue

Formal statement

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.MeanValue

theorem Rolles_Theorem (f : ℝ → ℝ) (a b : ℝ) (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfd : ∀ x ∈ Set.Ioo a b, DifferentiableAt ℝ f x) (hfab : f a = f b) : ∃ ξ ∈ Set.Ioo a b, deriv f ξ = 0 := by sorry

Source

https://proofwiki.org/wiki/Rolle%27s_Theorem

View graph