Theorems · Theorem · general topology

isLocalMax_of_mono_anti

∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {β : Type u_2}
  [inst_3 : Preorder β] {a b c : α},
  a < b → b < c → ∀ {f : α → β}, MonotoneOn f (Set.Ioc a b) → AntitoneOn f (Set.Ico b c) → IsLocalMax f b

If f is monotone on Ioc a b and antitone on Ico b c then f has a local maximum at b.

Defined in

Mathlib.Topology.Order.OrderClosedExtr

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLinearOrderOrderClosedTopologyPreorder