isExtrFilter_const

Mathlib.Order.Filter.Extr

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

English

The extremal-filter of a constant function is itself a constant extremum.

Русский

Экстремальный фильтр константной функции сохраняет константный экстремум.

LaTeX

$$$IsExtrFilter (fun _ => b) l a$$$

Lean4

theorem isExtrFilter_const {b : β} : IsExtrFilter (fun _ => b) l a :=
  isMinFilter_const.isExtr

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

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

Разделы

Аффилиация

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