isLocalMax — Mathlib

English

Let f: α → β be a function between preordered spaces, a ∈ α, and s ⊆ α. If a is a maximum of f on s and s is a neighborhood of a, then a is a local maximum of f.

Русский

Пусть f: α → β. Пусть a ∈ α и s ⊆ α. Если a является максимумом f на s и s содержит окрестность a, то в точке a функция имеет локальный максимум.

LaTeX

$$$\mathrm{IsMaxOn}(f,s,a) \land s \in \mathcal{N}(a) \Rightarrow \mathrm{IsLocalMax}(f,a)$$$

Lean4

theorem isLocalMax (hf : IsMaxOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMax f a :=
  hf.localize.isLocalMax hs

Похожие утверждения