congr — Mathlib

English

If f is locally extreme on s at a and f and g are eventually equal near a within s, then g is locally extreme on s at a.

Русский

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

LaTeX

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

Lean4

nonrec theorem congr {f g : α → β} {a : α} (h : IsLocalExtrOn f s a) (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) :
    IsLocalExtrOn g s a :=
  h.congr heq <| heq.eq_of_nhdsWithin hmem

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