compl_strictAnti

Mathlib.Order.Hom.Set

URI: https://scilib.ai/kg/mathlib#compl_strictAnti

English

The complementation map on a Boolean algebra is antitone: if a ≤ b then not a ≥ not b.

Русский

Операция дополнения по буловой алгебре антимонотонна: если a ≤ b, то не a ≥ не b.

LaTeX

$$$\forall a,b:\ a \le b \Rightarrow \mathrm{compl}(a) \ge \mathrm{compl}(b)$$$

Lean4

theorem compl_strictAnti : StrictAnti (compl : α → α) :=
  (OrderIso.compl α).strictMono

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

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

Разделы

Аффилиация

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