Theorems · Theorem · real analysis

exists_isLocalExtr_Ioo_of_tendsto

∀ {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} {l : Y},
  a < b →
    ContinuousOn f (Set.Ioo a b) →
      Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
        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.

Defined in

Mathlib.Topology.Order.Rolle

Cited by

1 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderDenselyOrderedTopologicalSpaceOrderTopologyLinearOrderTopologicalSpaceOrderTopology