isLocalMaxOn_univ_iff — Mathlib

English

There is an equivalence IsLocalMaxOn f univ a ⇔ IsLocalMax f a, i.e., local maximum on the whole space coincides with local maximum in general.

Русский

Существуют эквивалентности IsLocalMaxOn f univ a ⇔ IsLocalMax f a, то есть локальный максимум на всей системе совпадает с общим локальным максимумом.

LaTeX

$$$IsLocalMaxOn\ f\ {\text{univ}}\ a \leftrightarrow IsLocalMax f a$$$

Lean4

theorem isLocalMaxOn_univ_iff : IsLocalMaxOn f univ a ↔ IsLocalMax f a := by
  simp only [IsLocalMaxOn, IsLocalMax, nhdsWithin_univ]

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