English
If a and c provide left and right neighborhoods of b and f is monotone on a while antitone on c, then f has a local maximum at b.
Русский
Пусть b имеет окрестности слева и справа, обозначенные a и c, и функция f монотонна на a слева и Antitone на c справа; тогда f достигает локального максимума в b.
LaTeX
$$$\\forall {α} [TopologicalSpace α] [LinearOrder α] {β} [Preorder β] {b:\\alpha} {f: α \\to β} {a: Set α} (ha: a \\in 𝓝_{≤} b) {c: Set α} (hc: c \\in 𝓝_{≥} b) (h0: MonotoneOn f a) (h1: AntitoneOn f c) : IsLocalMax f b$$$
Lean4
/-- If `f` is monotone to the left and antitone to the right, then it has a local maximum. -/
theorem isLocalMax_of_mono_anti' {α : Type*} [TopologicalSpace α] [LinearOrder α] {β : Type*} [Preorder β] {b : α}
{f : α → β} {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b) (h₀ : MonotoneOn f a)
(h₁ : AntitoneOn f c) : IsLocalMax f b :=
have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)
