isLocalMinOn_iff — Mathlib

English

Two functions that are eventually equal near a within s have the same local maximality at a on s.

Русский

Две функции, которые совпадают почти в окрестности a внутри s, имеют одинаковый локальный максимум на s в a.

LaTeX

$$$\forall {f g: \alpha \to \beta} {a: \alpha} {s: Set\alpha},\; (nhdsWithin a s).EventuallyEq f g \to Set.instMembership.mem s a \to IsLocalMaxOn f s a \leftrightarrow IsLocalMaxOn g s a$$$

Lean4

nonrec theorem isLocalMinOn_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) :
    IsLocalMinOn f s a ↔ IsLocalMinOn g s a :=
  heq.isMinFilter_iff <| heq.eq_of_nhdsWithin hmem

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