compl_antitone — Mathlib

English

Another formulation: the complement is order-reversing; equality of inequalities is flipped under complement.

Русский

Другая формулировка: комплемента обращает порядок; неравенства меняют знак при переходе к дополнению.

LaTeX

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

Lean4

theorem compl_antitone : Antitone (compl : α → α) :=
  (OrderIso.compl α).monotone

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