filter_mono

Mathlib.Order.Filter.Extr

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

English

If a is a maximal element with respect to f on l, and l' ≤ l, then a remains maximal with respect to f on l'.

Русский

Если a максимален для f на l и l' ⊆ l, то a остаётся максимальным для f на l'.

LaTeX

$$$IsMaxFilter\ f\ l\ a \to Filter.instPartialOrder.le l' l \to IsMaxFilter\ f\ l'\ a$$$

Lean4

theorem filter_mono (h : IsMaxFilter f l a) (hl : l' ≤ l) : IsMaxFilter f l' a :=
  hl h

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

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

Разделы

Аффилиация

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