From 865e36bd919253936a710235c9e7f94cbcabb4b8 Mon Sep 17 00:00:00 2001 From: Eric Date: Sun, 18 Jul 2021 15:12:25 +0000 Subject: [PATCH] chore(order/boolean_algebra) : `compl_involutive` (#8357) Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com> --- src/order/boolean_algebra.lean | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/order/boolean_algebra.lean b/src/order/boolean_algebra.lean index fbc8040e4d0a2..3235f61098cdd 100644 --- a/src/order/boolean_algebra.lean +++ b/src/order/boolean_algebra.lean @@ -577,8 +577,13 @@ is_compl_bot_top.compl_eq @[simp] theorem compl_compl (x : α) : xᶜᶜ = x := is_compl_compl.symm.compl_eq +@[simp] theorem compl_involutive : function.involutive (compl : α → α) := compl_compl + +theorem compl_bijective : function.bijective (compl : α → α) := +compl_involutive.bijective + theorem compl_injective : function.injective (compl : α → α) := -function.involutive.injective compl_compl +compl_involutive.injective @[simp] theorem compl_inj_iff : xᶜ = yᶜ ↔ x = y := compl_injective.eq_iff