IsLocalMin — Mathlib

English

There exists a neighborhood of a where f(a) is less than or equal to f(x) for all x in that neighborhood; i.e., f(a) is minimal in some neighborhood of a.

Русский

Существует окрестность точки a, в которой значение f(a) не больше значений f(x) для всех x в этой окрестности.

LaTeX

$$$IsLocalMin f a$$$

Lean4

/-- `IsLocalMin f a` means that `f a ≤ f x` for all `x` in some neighborhood of `a`. -/
def IsLocalMin :=
  IsMinFilter f (𝓝 a) a

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