# Documentation

Mathlib.Topology.Algebra.Order.Rolle

# Rolle's Theorem (topological part) #

In this file we prove the purely topological part of Rolle's Theorem: a function that is continuous on an interval $[a, b]$, \$a

In Mathlib/Analysis/Calculus/LocalExtr/Rolle we use these lemmas to prove several versions of Rolle's Theorem from calculus.

## Keywords #

local minimum, local maximum, extremum, Rolle's Theorem

theorem exists_Ioo_extr_on_Icc {X : Type u_1} {Y : Type u_2} [] [] [] [] [] [] {f : XY} {a : X} {b : X} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) :
c, c Set.Ioo a b IsExtrOn f (Set.Icc a b) c

A continuous function on a closed interval with f a = f b takes either its maximum or its minimum value at a point in the interior of the interval.

theorem exists_isLocalExtr_Ioo {X : Type u_1} {Y : Type u_2} [] [] [] [] [] [] {f : XY} {a : X} {b : X} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) :
c, c Set.Ioo a b

A continuous function on a closed interval with f a = f b has a local extremum at some point of the corresponding open interval.

theorem exists_isExtrOn_Ioo_of_tendsto {X : Type u_1} {Y : Type u_2} [] [] [] [] [] [] {f : XY} {a : X} {b : X} {l : Y} (hab : a < b) (hfc : ContinuousOn f (Set.Ioo a b)) (ha : Filter.Tendsto f (nhdsWithin a ()) (nhds l)) (hb : Filter.Tendsto f (nhdsWithin b ()) (nhds l)) :
c, c Set.Ioo a b IsExtrOn f (Set.Ioo a b) c

If a function f is continuous on an open interval and tends to the same value at its endpoints, then it has an extremum on this open interval.

theorem exists_isLocalExtr_Ioo_of_tendsto {X : Type u_1} {Y : Type u_2} [] [] [] [] [] [] {f : XY} {a : X} {b : X} {l : Y} (hab : a < b) (hfc : ContinuousOn f (Set.Ioo a b)) (ha : Filter.Tendsto f (nhdsWithin a ()) (nhds l)) (hb : Filter.Tendsto f (nhdsWithin b ()) (nhds l)) :
c, c Set.Ioo a b

If a function f is continuous on an open interval and tends to the same value at its endpoints, then it has a local extremum on this open interval.