on — Mathlib · SciLib

English

If IsLocalExtr f a holds, then for any set s, IsLocalExtrOn f s a holds; local extremum persists under restriction to s.

Русский

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

LaTeX

$$$IsLocalExtr f a \rightarrow \forall s, IsLocalExtrOn f s a$$$

Lean4

theorem on (h : IsLocalExtr f a) (s) : IsLocalExtrOn f s a :=
  h.filter_inf _

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