Theorems · Theorem · real analysis

exists_Ioo_extr_on_Icc

∀ {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, 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.

Defined in

Mathlib.Topology.Order.Rolle

Cited by

3 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderDenselyOrderedTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology