congr — Mathlib

English

If f has a local minimum at a and f equals g near a in the nhds sense, then g has a local minimum at a.

Русский

Если у f есть локальный минимум в a и f близко к g вокруг a (в nhds), то у g также локальный минимум в a.

LaTeX

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

Lean4

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

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