on — Mathlib · SciLib

English

If IsLocalMin f a holds, then for any set s, IsLocalMinOn f s a holds; i.e., restricting the domain to s preserves a local minimum at a.

Русский

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

LaTeX

$$$IsLocalMin f a \rightarrow \forall s, IsLocalMinOn f s a$$$

Lean4

theorem on (h : IsLocalMin f a) (s) : IsLocalMinOn f s a :=
  h.filter_inf _

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