congr — Mathlib

English

If f is locally extreme at a and f equals g near a, then g is locally extreme at a.

Русский

Если f локально экстремальна в a и f равна g около a, то и g локально экстремальна в a.

LaTeX

$$$\\forall {f,g: \\alpha \\to \\beta}, {a:\\alpha}, IsLocalExtr f a \\Rightarrow (f =^{\\ NHds a}_{\\mathrm{ev}} g) \\Rightarrow IsLocalExtr g a$$$

Lean4

nonrec theorem congr {f g : α → β} {a : α} (h : IsLocalExtr f a) (heq : f =ᶠ[𝓝 a] g) : IsLocalExtr g a :=
  h.congr heq heq.eq_of_nhds

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