on_subset

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#IsExtrOn.on_subset

English

If a is extremal for f on t, and s ⊆ t, then a is extremal for f on s.

Русский

Если a экстремальна для f на t, и s ⊆ t, то a экстремальна для f на s.

LaTeX

$$$\text{IsExtrOn}(f,t,a) \land s\subseteq t \Rightarrow \text{IsExtrOn}(f,s,a)$$$

Lean4

theorem on_subset (hf : IsExtrOn f t a) (h : s ⊆ t) : IsExtrOn f s a :=
  hf.filter_mono <| principal_mono.2 h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru