filter_inf

Mathlib.Order.Filter.Extr

URI: https://scilib.ai/kg/mathlib#IsMaxFilter.filter_inf

English

If a is a maximum of f along l, then for any l', a is a maximum of f along l ⊓ l'.

Русский

Если a максимизирует f вдоль фильтра l, то для любого l' максимум достигается в a по лямбде l ⊓ l'.

LaTeX

$$$\text{IsMaxFilter}(f,l,a) \rightarrow \text{IsMaxFilter}(f,l\,\inf\,l',a)$$$

Lean4

theorem filter_inf (h : IsMaxFilter f l a) (l') : IsMaxFilter f (l ⊓ l') a :=
  h.filter_mono inf_le_left

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

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

Разделы

Аффилиация

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