Theorems · Theorem · real analysis

exists_isLocalExtr_Ioo

∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X},
  a < b → ContinuousOn f (Set.Icc a b) → 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.

Defined in

Mathlib.Topology.Order.Rolle

Cited by

3 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderDenselyOrderedTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology