Theorems · Theorem · general topology

isMaxOn_Iic_of_mono_anti

∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  MonotoneOn f (Set.Iic b) → AntitoneOn f (Set.Icc b a) → IsMaxOn f (Set.Iic a) b

If f is monotone on Iic b and antitone on Icc b a, then the maximum of f on Iic a is attained at b.

Defined in

Mathlib.Order.Filter.Extr

Cited by

2 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

LinearOrderPreorder