IsMinFilter — Mathlib

English

IsExtrFilter f l a means that f attains either a local minimum or a local maximum with respect to l at a.

Русский

IsExtrFilter f l a означает, что f достигает либо локального минимума, либо локального максимума относительно фильтра l в точке a.

LaTeX

$$$\mathrm{IsExtrFilter}(f,l,a) \iff \mathrm{IsMinFilter}(f,l,a) \lor \mathrm{IsMaxFilter}(f,l,a)$$$

Lean4

/-- `IsMinFilter f l a` means that `f a ≤ f x` for all `x` in some `l`-neighborhood of `a` -/
def IsMinFilter : Prop :=
  ∀ᶠ x in l, f a ≤ f x

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