IsLocalMaxOn — Mathlib

English

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

Русский

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

LaTeX

$$$ IsLocalMaxOn := IsMaxFilter\ f (nhdsWithin a s) a. $$$

Lean4

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

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