feat: The lattice of complemented elements

Match leanprover-community/mathlib#16267

Mathlib/Order/Disjoint.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module order.disjoint
-! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! leanprover-community/mathlib commit 22c4d2ff43714b6ff724b2745ccfdc0f236a4a76
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -25,6 +25,7 @@ This file defines `Disjoint`, `Codisjoint`, and the `IsCompl` predicate.
 
 -/
 
+open Function
 
 variable {α : Type _}
 
@@ -644,6 +645,39 @@ theorem eq_bot_of_top_isCompl (h : IsCompl ⊤ x) : x = ⊥ :=
 
 end
 
+section IsComplemented
+
+section Lattice
+
+variable [Lattice α] [BoundedOrder α]
+
+/-- An element is *complemented* if it has a complement. -/
+def IsComplemented (a : α) : Prop :=
+  ∃ b, IsCompl a b
+#align is_complemented IsComplemented
+
+theorem isComplemented_bot : IsComplemented (⊥ : α) :=
+  ⟨⊤, isCompl_bot_top⟩
+#align is_complemented_bot isComplemented_bot
+
+theorem isComplemented_top : IsComplemented (⊤ : α) :=
+  ⟨⊥, isCompl_top_bot⟩
+#align is_complemented_top isComplemented_top
+
+end Lattice
+
+variable [DistribLattice α] [BoundedOrder α] {a b : α}
+
+theorem IsComplemented.sup : IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b) :=
+  fun ⟨a', ha⟩ ⟨b', hb⟩ => ⟨a' ⊓ b', ha.sup_inf hb⟩
+#align is_complemented.sup IsComplemented.sup
+
+theorem IsComplemented.inf : IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b) :=
+  fun ⟨a', ha⟩ ⟨b', hb⟩ => ⟨a' ⊔ b', ha.inf_sup hb⟩
+#align is_complemented.inf IsComplemented.inf
+
+end IsComplemented
+
 /-- A complemented bounded lattice is one where every element has a (not necessarily unique)
 complement. -/
 class ComplementedLattice (α) [Lattice α] [BoundedOrder α] : Prop where
@@ -664,4 +698,107 @@ instance : ComplementedLattice αᵒᵈ :=
 
 end ComplementedLattice
 
+-- TODO: Define as a sublattice?
+/-- The sublattice of complemented elements. -/
+@[reducible]
+def Complementeds (α : Type _) [Lattice α] [BoundedOrder α] : Type _ := {a : α // IsComplemented a}
+#align complementeds Complementeds
+
+namespace Complementeds
+
+section Lattice
+
+variable [Lattice α] [BoundedOrder α] {a b : Complementeds α}
+
+instance hasCoeT : CoeTC (Complementeds α) α := ⟨Subtype.val⟩
+#align complementeds.has_coe_t Complementeds.hasCoeT
+
+theorem coe_injective : Injective ((↑) : Complementeds α → α) := Subtype.coe_injective
+#align complementeds.coe_injective Complementeds.coe_injective
+
+@[simp, norm_cast]
+theorem coe_inj : (a : α) = b ↔ a = b := Subtype.coe_inj
+#align complementeds.coe_inj Complementeds.coe_inj
+
+-- porting note: removing `simp` because `Subtype.coe_le_coe` already proves it
+@[norm_cast]
+theorem coe_le_coe : (a : α) ≤ b ↔ a ≤ b := by simp
+#align complementeds.coe_le_coe Complementeds.coe_le_coe
+
+-- porting note: removing `simp` because `Subtype.coe_lt_coe` already proves it
+@[norm_cast]
+theorem coe_lt_coe : (a : α) < b ↔ a < b := Iff.rfl
+#align complementeds.coe_lt_coe Complementeds.coe_lt_coe
+
+instance : BoundedOrder (Complementeds α) :=
+  Subtype.boundedOrder isComplemented_bot isComplemented_top
+
+@[simp, norm_cast]
+theorem coe_bot : ((⊥ : Complementeds α) : α) = ⊥ := rfl
+#align complementeds.coe_bot Complementeds.coe_bot
+
+@[simp, norm_cast]
+theorem coe_top : ((⊤ : Complementeds α) : α) = ⊤ := rfl
+#align complementeds.coe_top Complementeds.coe_top
+
+-- porting note: removing `simp` because `Subtype.mk_bot` already proves it
+theorem mk_bot : (⟨⊥, isComplemented_bot⟩ : Complementeds α) = ⊥ := rfl
+#align complementeds.mk_bot Complementeds.mk_bot
+
+-- porting note: removing `simp` because `Subtype.mk_top` already proves it
+theorem mk_top : (⟨⊤, isComplemented_top⟩ : Complementeds α) = ⊤ := rfl
+#align complementeds.mk_top Complementeds.mk_top
+
+instance : Inhabited (Complementeds α) := ⟨⊥⟩
+
+end Lattice
+
+variable [DistribLattice α] [BoundedOrder α] {a b : Complementeds α}
+
+instance : Sup (Complementeds α) :=
+  ⟨fun a b => ⟨a ⊔ b, a.2.sup b.2⟩⟩
+
+instance : Inf (Complementeds α) :=
+  ⟨fun a b => ⟨a ⊓ b, a.2.inf b.2⟩⟩
+
+@[simp, norm_cast]
+theorem coe_sup (a b : Complementeds α) : ↑(a ⊔ b) = (a : α) ⊔ b := rfl
+#align complementeds.coe_sup Complementeds.coe_sup
+
+@[simp, norm_cast]
+theorem coe_inf (a b : Complementeds α) : ↑(a ⊓ b) = (a : α) ⊓ b := rfl
+#align complementeds.coe_inf Complementeds.coe_inf
+
+@[simp]
+theorem mk_sup_mk {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
+    (⟨a, ha⟩ ⊔ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊔ b, ha.sup hb⟩ := rfl
+#align complementeds.mk_sup_mk Complementeds.mk_sup_mk
+
+@[simp]
+theorem mk_inf_mk {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
+    (⟨a, ha⟩ ⊓ ⟨b, hb⟩ : Complementeds α) = ⟨a ⊓ b, ha.inf hb⟩ := rfl
+#align complementeds.mk_inf_mk Complementeds.mk_inf_mk
+
+instance : DistribLattice (Complementeds α) :=
+  Complementeds.coe_injective.distribLattice _ coe_sup coe_inf
+
+@[simp, norm_cast]
+theorem disjoint_coe : Disjoint (a : α) b ↔ Disjoint a b := by
+  rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
+#align complementeds.disjoint_coe Complementeds.disjoint_coe
+
+@[simp, norm_cast]
+theorem codisjoint_coe : Codisjoint (a : α) b ↔ Codisjoint a b := by
+  rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
+#align complementeds.codisjoint_coe Complementeds.codisjoint_coe
+
+@[simp, norm_cast]
+theorem isCompl_coe : IsCompl (a : α) b ↔ IsCompl a b := by
+  simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]
+#align complementeds.is_compl_coe Complementeds.isCompl_coe
+
+instance : ComplementedLattice (Complementeds α) :=
+  ⟨fun ⟨a, b, h⟩ => ⟨⟨b, a, h.symm⟩, isCompl_coe.1 h⟩⟩
+
+end Complementeds
 end IsCompl