English
If a < b < c and f is monotone on (a,b] and antitone on [b,c), then f has a local maximum at b.
Русский
Если a < b < c и f монотонна на (a,b], антимонотонна на [b,c), тогда в точке b функция достигает локального максимума.
LaTeX
$$$a < b < c \Rightarrow (\text{MonotoneOn } f (Ioc\ a\ b)) \land (\text{AntitoneOn } f (Ico\ b\ c)) \Rightarrow \text{IsLocalMax } f\ b.$$$
Lean4
/-- If `f` is monotone on `(a,b]` and antitone on `[b,c)` then `f` has
a local maximum at `b`. -/
theorem isLocalMax_of_mono_anti {α : Type*} [TopologicalSpace α] [LinearOrder α] [OrderClosedTopology α] {β : Type*}
[Preorder β] {a b c : α} (g₀ : a < b) (g₁ : b < c) {f : α → β} (h₀ : MonotoneOn f (Ioc a b))
(h₁ : AntitoneOn f (Ico b c)) : IsLocalMax f b :=
isLocalMax_of_mono_anti' (Ioc_mem_nhdsLE g₀) (Ico_mem_nhdsGE g₁) h₀ h₁
