Documentation

Mathlib.Order.Disjoint

Disjointness and complements #

This file defines Disjoint, Codisjoint, and the IsCompl predicate.

Main declarations #

def Disjoint {α : Type u_1} [PartialOrder α] [OrderBot α] (a : α) (b : α) :

Two elements of a lattice are disjoint if their inf is the bottom element. (This generalizes disjoint sets, viewed as members of the subset lattice.)

Note that we define this without reference to , as this allows us to talk about orders where the infimum is not unique, or where implementing Inf would require additional Decidable arguments.

Equations
Instances For
    @[simp]
    theorem disjoint_of_subsingleton {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} [Subsingleton α] :
    theorem disjoint_comm {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} :
    theorem Disjoint.symm {α : Type u_1} [PartialOrder α] [OrderBot α] ⦃a : α ⦃b : α :
    Disjoint a bDisjoint b a
    theorem symmetric_disjoint {α : Type u_1} [PartialOrder α] [OrderBot α] :
    Symmetric Disjoint
    @[simp]
    theorem disjoint_bot_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
    @[simp]
    theorem disjoint_bot_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
    theorem Disjoint.mono {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
    Disjoint b dDisjoint a c
    theorem Disjoint.mono_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} {c : α} (h : a b) :
    Disjoint b cDisjoint a c
    theorem Disjoint.mono_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} {c : α} :
    b cDisjoint a cDisjoint a b
    @[simp]
    theorem disjoint_self {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
    theorem Disjoint.eq_bot_of_self {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
    Disjoint a aa =

    Alias of the forward direction of disjoint_self.

    theorem Disjoint.ne {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} (ha : a ) (hab : Disjoint a b) :
    a b
    theorem Disjoint.eq_bot_of_le {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hab : Disjoint a b) (h : a b) :
    a =
    theorem Disjoint.eq_bot_of_ge {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hab : Disjoint a b) :
    b ab =
    theorem Disjoint.eq_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hab : Disjoint a b) :
    a = b a = b =
    theorem Disjoint.ne_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} {b : α} (hab : Disjoint a b) :
    a b a b
    @[simp]
    theorem disjoint_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
    @[simp]
    theorem top_disjoint {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
    theorem disjoint_iff_inf_le {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} :
    theorem disjoint_iff {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} :
    Disjoint a b a b =
    theorem Disjoint.le_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} :
    Disjoint a ba b
    theorem Disjoint.eq_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} :
    Disjoint a ba b =
    theorem disjoint_assoc {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} {c : α} :
    Disjoint (a b) c Disjoint a (b c)
    theorem disjoint_left_comm {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} {c : α} :
    Disjoint a (b c) Disjoint b (a c)
    theorem disjoint_right_comm {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} {c : α} :
    Disjoint (a b) c Disjoint (a c) b
    theorem Disjoint.inf_left {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
    Disjoint (a c) b
    theorem Disjoint.inf_left' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
    Disjoint (c a) b
    theorem Disjoint.inf_right {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
    Disjoint a (b c)
    theorem Disjoint.inf_right' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
    Disjoint a (c b)
    theorem Disjoint.of_disjoint_inf_of_le {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} {c : α} (h : Disjoint (a b) c) (hle : a c) :
    theorem Disjoint.of_disjoint_inf_of_le' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} {c : α} (h : Disjoint (a b) c) (hle : b c) :
    theorem Disjoint.right_lt_sup_of_left_ne_bot {α : Type u_1} [SemilatticeSup α] [OrderBot α] {a : α} {b : α} (h : Disjoint a b) (ha : a ) :
    b < a b
    @[simp]
    theorem disjoint_sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {c : α} :
    @[simp]
    theorem disjoint_sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {c : α} :
    theorem Disjoint.sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
    Disjoint (a b) c
    theorem Disjoint.sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {c : α} (hb : Disjoint a b) (hc : Disjoint a c) :
    Disjoint a (b c)
    theorem Disjoint.left_le_of_le_sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {c : α} (h : a b c) (hd : Disjoint a c) :
    a b
    theorem Disjoint.left_le_of_le_sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a : α} {b : α} {c : α} (h : a c b) (hd : Disjoint a c) :
    a b
    def Codisjoint {α : Type u_1} [PartialOrder α] [OrderTop α] (a : α) (b : α) :

    Two elements of a lattice are codisjoint if their sup is the top element.

    Note that we define this without reference to , as this allows us to talk about orders where the supremum is not unique, or where implement Sup would require additional Decidable arguments.

    Equations
    Instances For
      theorem Codisjoint_comm {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} :
      theorem Codisjoint.symm {α : Type u_1} [PartialOrder α] [OrderTop α] ⦃a : α ⦃b : α :
      theorem symmetric_codisjoint {α : Type u_1} [PartialOrder α] [OrderTop α] :
      Symmetric Codisjoint
      @[simp]
      theorem codisjoint_top_left {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
      @[simp]
      theorem codisjoint_top_right {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
      theorem Codisjoint.mono {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
      theorem Codisjoint.mono_left {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} {c : α} (h : a b) :
      theorem Codisjoint.mono_right {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} {c : α} :
      b cCodisjoint a bCodisjoint a c
      @[simp]
      theorem codisjoint_self {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
      theorem Codisjoint.eq_top_of_self {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
      Codisjoint a aa =

      Alias of the forward direction of codisjoint_self.

      theorem Codisjoint.ne {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} (ha : a ) (hab : Codisjoint a b) :
      a b
      theorem Codisjoint.eq_top_of_le {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) (h : b a) :
      a =
      theorem Codisjoint.eq_top_of_ge {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) :
      a bb =
      theorem Codisjoint.eq_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) :
      a = b a = b =
      theorem Codisjoint.ne_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) :
      a b a b
      @[simp]
      theorem codisjoint_bot {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
      @[simp]
      theorem bot_codisjoint {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
      theorem Codisjoint.ne_bot_of_ne_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} {b : α} (h : Codisjoint a b) (ha : a ) :
      theorem Codisjoint.ne_bot_of_ne_top' {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} {b : α} (h : Codisjoint a b) (hb : b ) :
      theorem codisjoint_iff_le_sup {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} :
      theorem codisjoint_iff {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} :
      theorem Codisjoint.top_le {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} :
      Codisjoint a b a b
      theorem Codisjoint.eq_top {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} :
      Codisjoint a ba b =
      theorem codisjoint_assoc {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} {c : α} :
      Codisjoint (a b) c Codisjoint a (b c)
      theorem codisjoint_left_comm {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} {c : α} :
      Codisjoint a (b c) Codisjoint b (a c)
      theorem codisjoint_right_comm {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} {c : α} :
      Codisjoint (a b) c Codisjoint (a c) b
      theorem Codisjoint.sup_left {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
      Codisjoint (a c) b
      theorem Codisjoint.sup_left' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
      Codisjoint (c a) b
      theorem Codisjoint.sup_right {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
      Codisjoint a (b c)
      theorem Codisjoint.sup_right' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
      Codisjoint a (c b)
      theorem Codisjoint.of_codisjoint_sup_of_le {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} {c : α} (h : Codisjoint (a b) c) (hle : c a) :
      theorem Codisjoint.of_codisjoint_sup_of_le' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} {c : α} (h : Codisjoint (a b) c) (hle : c b) :
      @[simp]
      theorem codisjoint_inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a : α} {b : α} {c : α} :
      @[simp]
      theorem codisjoint_inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a : α} {b : α} {c : α} :
      theorem Codisjoint.inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a : α} {b : α} {c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) :
      Codisjoint (a b) c
      theorem Codisjoint.inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a : α} {b : α} {c : α} (hb : Codisjoint a b) (hc : Codisjoint a c) :
      Codisjoint a (b c)
      theorem Codisjoint.left_le_of_le_inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a : α} {b : α} {c : α} (h : a b c) (hd : Codisjoint b c) :
      a c
      theorem Codisjoint.left_le_of_le_inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a : α} {b : α} {c : α} (h : b a c) (hd : Codisjoint b c) :
      a c
      theorem Disjoint.dual {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} :
      Disjoint a bCodisjoint (OrderDual.toDual a) (OrderDual.toDual b)
      theorem Codisjoint.dual {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} :
      Codisjoint a bDisjoint (OrderDual.toDual a) (OrderDual.toDual b)
      @[simp]
      theorem disjoint_toDual_iff {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : α} {b : α} :
      Disjoint (OrderDual.toDual a) (OrderDual.toDual b) Codisjoint a b
      @[simp]
      theorem disjoint_ofDual_iff {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : αᵒᵈ} {b : αᵒᵈ} :
      Disjoint (OrderDual.ofDual a) (OrderDual.ofDual b) Codisjoint a b
      @[simp]
      theorem codisjoint_toDual_iff {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a : α} {b : α} :
      Codisjoint (OrderDual.toDual a) (OrderDual.toDual b) Disjoint a b
      @[simp]
      theorem codisjoint_ofDual_iff {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a : αᵒᵈ} {b : αᵒᵈ} :
      Codisjoint (OrderDual.ofDual a) (OrderDual.ofDual b) Disjoint a b
      theorem Disjoint.le_of_codisjoint {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : α} {b : α} {c : α} (hab : Disjoint a b) (hbc : Codisjoint b c) :
      a c
      structure IsCompl {α : Type u_1} [PartialOrder α] [BoundedOrder α] (x : α) (y : α) :

      Two elements x and y are complements of each other if x ⊔ y = ⊤ and x ⊓ y = ⊥.

      • disjoint : Disjoint x y

        If x and y are to be complementary in an order, they should be disjoint.

      • codisjoint : Codisjoint x y

        If x and y are to be complementary in an order, they should be codisjoint.

      Instances For
        theorem IsCompl.disjoint {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x : α} {y : α} (self : IsCompl x y) :

        If x and y are to be complementary in an order, they should be disjoint.

        theorem IsCompl.codisjoint {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x : α} {y : α} (self : IsCompl x y) :

        If x and y are to be complementary in an order, they should be codisjoint.

        theorem isCompl_iff {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} {b : α} :
        theorem IsCompl.symm {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
        theorem isCompl_comm {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x : α} {y : α} :
        theorem IsCompl.dual {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
        IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
        theorem IsCompl.ofDual {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : αᵒᵈ} {b : αᵒᵈ} (h : IsCompl a b) :
        IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b)
        theorem IsCompl.of_le {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} {y : α} (h₁ : x y ) (h₂ : x y) :
        theorem IsCompl.of_eq {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} {y : α} (h₁ : x y = ) (h₂ : x y = ) :
        theorem IsCompl.inf_eq_bot {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
        x y =
        theorem IsCompl.sup_eq_top {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
        x y =
        theorem IsCompl.inf_left_le_of_le_sup_right {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : α} {b : α} {x : α} {y : α} (h : IsCompl x y) (hle : a b y) :
        a x b
        theorem IsCompl.le_sup_right_iff_inf_left_le {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {a : α} {b : α} (h : IsCompl x y) :
        a b y a x b
        theorem IsCompl.inf_left_eq_bot_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
        x y = x z
        theorem IsCompl.inf_right_eq_bot_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
        x z = x y
        theorem IsCompl.disjoint_left_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
        Disjoint x y x z
        theorem IsCompl.disjoint_right_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
        Disjoint x z x y
        theorem IsCompl.le_left_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
        z x Disjoint z y
        theorem IsCompl.le_right_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
        z y Disjoint z x
        theorem IsCompl.left_le_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
        theorem IsCompl.right_le_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
        theorem IsCompl.Antitone {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {x' : α} {y' : α} (h : IsCompl x y) (h' : IsCompl x' y') (hx : x x') :
        y' y
        theorem IsCompl.right_unique {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (hxy : IsCompl x y) (hxz : IsCompl x z) :
        y = z
        theorem IsCompl.left_unique {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {z : α} (hxz : IsCompl x z) (hyz : IsCompl y z) :
        x = y
        theorem IsCompl.sup_inf {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {x' : α} {y' : α} (h : IsCompl x y) (h' : IsCompl x' y') :
        IsCompl (x x') (y y')
        theorem IsCompl.inf_sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x : α} {y : α} {x' : α} {y' : α} (h : IsCompl x y) (h' : IsCompl x' y') :
        IsCompl (x x') (y y')
        theorem Prod.disjoint_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] {x : α × β} {y : α × β} :
        Disjoint x y Disjoint x.1 y.1 Disjoint x.2 y.2
        theorem Prod.codisjoint_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] {x : α × β} {y : α × β} :
        Codisjoint x y Codisjoint x.1 y.1 Codisjoint x.2 y.2
        theorem Prod.isCompl_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] {x : α × β} {y : α × β} :
        IsCompl x y IsCompl x.1 y.1 IsCompl x.2 y.2
        @[simp]
        theorem isCompl_toDual_iff {α : Type u_1} [Lattice α] [BoundedOrder α] {a : α} {b : α} :
        IsCompl (OrderDual.toDual a) (OrderDual.toDual b) IsCompl a b
        @[simp]
        theorem isCompl_ofDual_iff {α : Type u_1} [Lattice α] [BoundedOrder α] {a : αᵒᵈ} {b : αᵒᵈ} :
        IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b) IsCompl a b
        theorem eq_top_of_isCompl_bot {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x ) :
        x =
        theorem eq_top_of_bot_isCompl {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x) :
        x =
        theorem eq_bot_of_isCompl_top {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x ) :
        x =
        theorem eq_bot_of_top_isCompl {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x) :
        x =
        def IsComplemented {α : Type u_1} [Lattice α] [BoundedOrder α] (a : α) :

        An element is complemented if it has a complement.

        Equations
        Instances For
          theorem IsComplemented.sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : α} {b : α} :
          theorem IsComplemented.inf {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : α} {b : α} :
          class ComplementedLattice (α : Type u_2) [Lattice α] [BoundedOrder α] :

          A complemented bounded lattice is one where every element has a (not necessarily unique) complement.

          Instances
            theorem ComplementedLattice.exists_isCompl {α : Type u_2} :
            ∀ {inst : Lattice α} {inst_1 : BoundedOrder α} [self : ComplementedLattice α] (a : α), ∃ (b : α), IsCompl a b

            In a ComplementedLattice, every element admits a complement.

            theorem complementedLattice_iff (α : Type u_2) [Lattice α] [BoundedOrder α] :
            ComplementedLattice α ∀ (a : α), ∃ (b : α), IsCompl a b
            @[reducible, inline]
            abbrev Complementeds (α : Type u_2) [Lattice α] [BoundedOrder α] :
            Type u_2

            The sublattice of complemented elements.

            Equations
            Instances For
              instance Complementeds.hasCoeT {α : Type u_1} [Lattice α] [BoundedOrder α] :
              Equations
              • Complementeds.hasCoeT = { coe := Subtype.val }
              @[simp]
              theorem Complementeds.coe_inj {α : Type u_1} [Lattice α] [BoundedOrder α] {a : Complementeds α} {b : Complementeds α} :
              a = b a = b
              theorem Complementeds.coe_le_coe {α : Type u_1} [Lattice α] [BoundedOrder α] {a : Complementeds α} {b : Complementeds α} :
              a b a b
              theorem Complementeds.coe_lt_coe {α : Type u_1} [Lattice α] [BoundedOrder α] {a : Complementeds α} {b : Complementeds α} :
              a < b a < b
              Equations
              @[simp]
              theorem Complementeds.coe_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
              =
              @[simp]
              theorem Complementeds.coe_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
              =
              theorem Complementeds.mk_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
              , =
              theorem Complementeds.mk_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
              , =
              Equations
              • Complementeds.instInhabited = { default := }
              Equations
              • Complementeds.instSup = { sup := fun (a b : Complementeds α) => a b, }
              Equations
              • Complementeds.instInf = { inf := fun (a b : Complementeds α) => a b, }
              @[simp]
              theorem Complementeds.coe_sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a : Complementeds α) (b : Complementeds α) :
              (a b) = a b
              @[simp]
              theorem Complementeds.coe_inf {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a : Complementeds α) (b : Complementeds α) :
              (a b) = a b
              @[simp]
              theorem Complementeds.mk_sup_mk {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : α} {b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
              a, ha b, hb = a b,
              @[simp]
              theorem Complementeds.mk_inf_mk {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : α} {b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
              a, ha b, hb = a b,
              Equations
              @[simp]
              theorem Complementeds.disjoint_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : Complementeds α} {b : Complementeds α} :
              Disjoint a b Disjoint a b
              @[simp]
              @[simp]
              theorem Complementeds.isCompl_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a : Complementeds α} {b : Complementeds α} :
              IsCompl a b IsCompl a b