isExtr

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#IsMaxOn.isExtr

English

The constant function is extremal on any set at any point.

Русский

Постоянная функция является экстремальной на любом множестве в любой точке.

LaTeX

$$$IsExtrOn (fun _ => b) s a \iff \text{(isExtrOn for constant function)}$$$

Lean4

theorem isExtr (h : IsMaxOn f s a) : IsExtrOn f s a :=
  IsMaxFilter.isExtr h

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

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

Разделы

Аффилиация

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