English
If f is antitone on a left neighborhood and monotone on a right neighborhood of b, then f has a local minimum at b.
Русский
Если f антимонотонна слева и монотонна справа вокруг точки b, то в точке b функция достигает локального минимума.
LaTeX
$$$\\forall {α} [TopologicalSpace α] [LinearOrder α] {β} [Preorder β] {b:\\alpha} {f: α \\to β} {a: Set α} (ha: a \\in 𝓝_{≤} b) {c: Set α} (hc: c \\in 𝓝_{≥} b) (h0: AntitoneOn f a) (h1: MonotoneOn f c) : IsLocalMin f b$$$
Lean4
/-- If `f` is antitone to the left and monotone to the right, then it has a local minimum. -/
theorem isLocalMin_of_anti_mono' {α : Type*} [TopologicalSpace α] [LinearOrder α] {β : Type*} [Preorder β] {b : α}
{f : α → β} {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b) (h₀ : AntitoneOn f a)
(h₁ : MonotoneOn f c) : IsLocalMin 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)
