isLocalMax_iff — Mathlib

English

If two functions f and g are Eventually Equal near a, then f has a local maximum at a if and only if g has a local maximum at a.

Русский

Если две функции f и g равны на окрестности точки a до какого-либо момента (EventuallyEq near a), то f имеет локальный максимум в a тогда и только тогда, когда g имеет локальный максимум в a.

LaTeX

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

Lean4

theorem isLocalMax_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalMax f a ↔ IsLocalMax g a :=
  heq.isMaxFilter_iff heq.eq_of_nhds

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