on — Mathlib · SciLib

English

If IsLocalMax f a holds, then for any s, IsLocalMaxOn f s a holds; restricting the domain to s preserves a local maximum at a.

Русский

Если IsLocalMax f a выполняется, то для любого s выполняется IsLocalMaxOn f s a; ограничение области до s сохраняет локальный максимум в a.

LaTeX

$$$IsLocalMax f a \rightarrow \forall s, IsLocalMaxOn f s a$$$

Lean4

theorem on (h : IsLocalMax f a) (s) : IsLocalMaxOn f s a :=
  h.filter_inf _

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