neg

Mathlib.Order.Filter.Extr

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

English

If f is maximal, then −f is minimal after negation.

Русский

Если f максимум, то после отрицания −f минимален.

LaTeX

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

Lean4

theorem neg (hf : IsMinOn f s a) : IsMaxOn (fun x => -f x) s a :=
  hf.comp_antitone fun _x _y hx => neg_le_neg hx

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

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

Разделы

Аффилиация

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