neg

Mathlib.Order.Filter.Extr

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

English

If f is maximal, then the negation −f is minimal (when negation is defined).

Русский

Если f максимален, то отрицание −f минимально (при условии существования определения отрицания).

LaTeX

$$$hf : IsMaxFilter f l a \Rightarrow IsMinFilter (-f) l a$$$

Lean4

theorem neg (hf : IsMaxFilter f l a) : IsMinFilter (fun x => -f x) l a :=
  hf.comp_antitone fun _x _y hx => neg_le_neg hx

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

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

Разделы

Аффилиация

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