neg — Mathlib

English

If f is minimal, then the negation −f is maximal (when the ambient structure supports negation).

Русский

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

LaTeX

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

Lean4

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

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