isExtrOn_const

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#isExtrOn_const

English

The constant function yields an extremal-on property on any s at any a.

Русский

Константная функция задаёт экстремум на любом s в любой точке a.

LaTeX

$$$IsExtrOn (fun _ => b) s a$$$

Lean4

theorem isExtrOn_const {b : β} : IsExtrOn (fun _ => b) s a :=
  isExtrFilter_const

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

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

Разделы

Аффилиация

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