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 < b$, has a local extremum at a point $x ∈ (a, b)$ provided that $f(a)=f(b)$. We also prove several variations of this statement.

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} [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X] [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {a b : X} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) : ∃ 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} [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X] [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {a b : X} (hab : a < b) (hfc : ContinuousOn f (Set.Icc a b)) (hfI : f a = f b) : ∃ c ∈ Set.Ioo a b, IsLocalExtr f c

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} [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X] [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {a b : X} {l : Y} (hab : a < b) (hfc : ContinuousOn f (Set.Ioo a b)) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l)) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l)) : ∃ 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} [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X] [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y] {f : X → Y} {a b : X} {l : Y} (hab : a < b) (hfc : ContinuousOn f (Set.Ioo a b)) (ha : Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l)) (hb : Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l)) : ∃ c ∈ Set.Ioo a b, IsLocalExtr f c

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.