isLocalMaxOn_iff — Mathlib

English

If f and g are eventually equal near a in s and f has a local minimum on s at a, then g has a local minimum on s at a, given the equality of neighborhoods.

Русский

Если f и g совпадают вплоть до окрестности около a в s, и f имеет локальный минимум на s в a, то у g тоже локальный минимум, при условии совпадения окрестностей.

LaTeX

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

Lean4

theorem isLocalMaxOn_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) :
    IsLocalMaxOn f s a ↔ IsLocalMaxOn g s a :=
  heq.isMaxFilter_iff <| heq.eq_of_nhdsWithin hmem

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