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
      @[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
      theorem disjoint_of_le_iff_left_eq_bot {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (h : 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 : α} :
      Disjoint a b ab
      theorem disjoint_iff {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
      Disjoint a b ab =
      theorem Disjoint.le_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
      Disjoint a bab
      theorem Disjoint.eq_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
      Disjoint a bab =
      theorem disjoint_assoc {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} :
      Disjoint (ab) c Disjoint a (bc)
      theorem disjoint_left_comm {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} :
      Disjoint a (bc) Disjoint b (ac)
      theorem disjoint_right_comm {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} :
      Disjoint (ab) c Disjoint (ac) b
      theorem Disjoint.inf_left {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
      Disjoint (ac) b
      theorem Disjoint.inf_left' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
      Disjoint (ca) b
      theorem Disjoint.inf_right {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
      Disjoint a (bc)
      theorem Disjoint.inf_right' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
      Disjoint a (cb)
      theorem Disjoint.of_disjoint_inf_of_le {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} (h : Disjoint (ab) c) (hle : a c) :
      theorem Disjoint.of_disjoint_inf_of_le' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} (h : Disjoint (ab) 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 < ab
      @[simp]
      theorem disjoint_sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} :
      Disjoint (ab) c Disjoint a c Disjoint b c
      @[simp]
      theorem disjoint_sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} :
      Disjoint a (bc) Disjoint a b Disjoint a c
      theorem Disjoint.sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
      Disjoint (ab) c
      theorem Disjoint.sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} (hb : Disjoint a b) (hc : Disjoint a c) :
      Disjoint a (bc)
      theorem Disjoint.left_le_of_le_sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} (h : a bc) (hd : Disjoint a c) :
      a b
      theorem Disjoint.left_le_of_le_sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} (h : a cb) (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 : α} :
          @[deprecated codisjoint_comm (since := "2024-11-23")]
          theorem Codisjoint_comm {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} :

          Alias of codisjoint_comm.

          theorem Codisjoint.symm {α : Type u_1} [PartialOrder α] [OrderTop α] a b : α :
          @[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 : α} :
          Codisjoint a b ab
          theorem codisjoint_iff {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
          Codisjoint a b ab =
          theorem Codisjoint.top_le {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
          Codisjoint a b ab
          theorem Codisjoint.eq_top {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
          Codisjoint a bab =
          theorem codisjoint_assoc {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} :
          Codisjoint (ab) c Codisjoint a (bc)
          theorem codisjoint_left_comm {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} :
          Codisjoint a (bc) Codisjoint b (ac)
          theorem codisjoint_right_comm {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} :
          Codisjoint (ab) c Codisjoint (ac) b
          theorem Codisjoint.sup_left {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
          Codisjoint (ac) b
          theorem Codisjoint.sup_left' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
          Codisjoint (ca) b
          theorem Codisjoint.sup_right {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
          Codisjoint a (bc)
          theorem Codisjoint.sup_right' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
          Codisjoint a (cb)
          theorem Codisjoint.of_codisjoint_sup_of_le {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} (h : Codisjoint (ab) c) (hle : c a) :
          theorem Codisjoint.of_codisjoint_sup_of_le' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} (h : Codisjoint (ab) c) (hle : c b) :
          @[simp]
          theorem codisjoint_inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} :
          Codisjoint (ab) c Codisjoint a c Codisjoint b c
          @[simp]
          theorem codisjoint_inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} :
          Codisjoint a (bc) Codisjoint a b Codisjoint a c
          theorem Codisjoint.inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) :
          Codisjoint (ab) c
          theorem Codisjoint.inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} (hb : Codisjoint a b) (hc : Codisjoint a c) :
          Codisjoint a (bc)
          theorem Codisjoint.left_le_of_le_inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} (h : ab c) (hd : Codisjoint b c) :
          a c
          theorem Codisjoint.left_le_of_le_inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} (h : ba c) (hd : Codisjoint b c) :
          a c
          theorem Disjoint.dual {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} :
          theorem Codisjoint.dual {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} :
          @[simp]
          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_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) :
            theorem IsCompl.of_le {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : xy ) (h₂ : xy) :
            theorem IsCompl.of_eq {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : xy = ) (h₂ : xy = ) :
            theorem IsCompl.inf_eq_bot {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h : IsCompl x y) :
            xy =
            theorem IsCompl.sup_eq_top {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h : IsCompl x y) :
            xy =
            theorem IsCompl.inf_left_le_of_le_sup_right {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b x y : α} (h : IsCompl x y) (hle : a by) :
            ax b
            theorem IsCompl.le_sup_right_iff_inf_left_le {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y a b : α} (h : IsCompl x y) :
            a by ax b
            theorem IsCompl.inf_left_eq_bot_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) :
            xy = x z
            theorem IsCompl.inf_right_eq_bot_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) :
            xz = 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 (xx') (yy')
            theorem IsCompl.inf_sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y x' y' : α} (h : IsCompl x y) (h' : IsCompl x' y') :
            IsCompl (xx') (yy')
            theorem Prod.disjoint_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] {x y : α × β} :
            theorem Prod.codisjoint_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] {x y : α × β} :
            theorem Prod.isCompl_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] {x y : α × β} :
            @[simp]
            theorem isCompl_toDual_iff {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α} :
            @[simp]
            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_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
                        @[simp]
                        theorem Complementeds.coe_inj {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : Complementeds α} :
                        a = b a = b
                        theorem Complementeds.coe_le_coe {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : Complementeds α} :
                        a b a b
                        theorem Complementeds.coe_lt_coe {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : Complementeds α} :
                        a < b a < b
                        @[simp]
                        theorem Complementeds.coe_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
                        =
                        @[simp]
                        theorem Complementeds.coe_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
                        =
                        Equations
                          Equations
                            @[simp]
                            theorem Complementeds.coe_sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a b : Complementeds α) :
                            (ab) = ab
                            @[simp]
                            theorem Complementeds.coe_inf {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a b : Complementeds α) :
                            (ab) = ab
                            @[simp]
                            theorem Complementeds.mk_sup_mk {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
                            a, hab, hb = ab,
                            @[simp]
                            theorem Complementeds.mk_inf_mk {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : α} (ha : IsComplemented a) (hb : IsComplemented b) :
                            a, hab, hb = ab,
                            @[simp]
                            theorem Complementeds.disjoint_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : Complementeds α} :
                            Disjoint a b Disjoint a b
                            @[simp]
                            @[simp]
                            theorem Complementeds.isCompl_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : Complementeds α} :
                            IsCompl a b IsCompl a b