Theorems · Theorem · real analysis

exists_isLocalExtr_uIoo

∀ {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.uIcc a b) → f a = f b → ∃ c ∈ Set.uIoo a b, IsLocalExtr f c

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

Defined in

Mathlib.Topology.Order.Rolle

Cited by

0 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderDenselyOrderedTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology