IsLocalMax — Mathlib

English

There exists a neighborhood of a where f(x) ≤ f(a) for all x in that neighborhood; equivalently, f(a) is maximal in some neighborhood of a.

Русский

Существует окрестность точки a, в которой для всех x выполнено f(x) ≤ f(a); то есть f(a) достигает локального максимума.

LaTeX

$$$IsLocalMax f a$$$

Lean4

/-- `IsLocalMax f a` means that `f x ≤ f a` for all `x ∈ s` in some neighborhood of `a`. -/
def IsLocalMax :=
  IsMaxFilter f (𝓝 a) a

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