Complement is strictly antitone

Stream: Is there code for X?

[Markus Himmel]

Is one of these in mathlib somewhere?

import order.boolean_algebra

lemma strict_anti_compl {α : Type*} [boolean_algebra.core α] : strict_anti (compl : α → α) :=
λ x y h, lt_of_le_of_ne (is_compl_compl.antitone is_compl_compl $ le_of_lt h) $ λ h', ne_of_lt h $ compl_inj_iff.mp h'.symm

lemma antitone_compl {α : Type*} [boolean_algebra.core α] : antitone (compl : α → α) :=
strict_anti_compl.antitone

[Yaël Dillies]

The second one, yes, as docs#compl_le_compl. You can deduce the first one easily from docs#compl_le_compl_iff_le.

[Yaël Dillies]

The best would be to bundle compl as a α ≃o order_dual α (docs#order_iso).

[Yaël Dillies]

And then you can deduce antitonicity and strict antitonicity as one-liners.

[Markus Himmel]

Nice idea. I opened #11630.