IsLocalMinOn — Mathlib

English

IsLocalMinOn f s a means that f(a) ≤ f(x) for all x in s in some neighborhood of a.

Русский

IsLocalMinOn f s a означает, что существует окрестность a в которой для всех x ∈ s выполняется f(a) ≤ f(x).

LaTeX

$$$ IsLocalMinOn := IsMinFilter\ f (nhdsWithin a s) a. $$$

Lean4

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

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