feat(order/rel_classes): Reflexive relation from irreflexive and vice…

…versa (#13411)
leanprover-community · May 26, 2022 · 525cc65 · 525cc65
1 parent b2973b1
commit 525cc65
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/order/boolean_algebra.lean b/src/order/boolean_algebra.lean
@@ -812,6 +812,9 @@ instance pi.has_compl {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i
 lemma pi.compl_def {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] (x : Π i, α i) :
   xᶜ = λ i, (x i)ᶜ := rfl
 
+instance is_irrefl.compl (r) [is_irrefl α r] : is_refl α rᶜ := ⟨@irrefl α r _⟩
+instance is_refl.compl (r) [is_refl α r] : is_irrefl α rᶜ := ⟨λ a, not_not_intro (refl a)⟩
+
 @[simp]
 lemma pi.compl_apply {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] (x : Π i, α i) (i : ι)  :
   xᶜ i = (x i)ᶜ := rfl