Documentation

Mathlib.Order.Disjoint

Disjointness and complements #

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

Main declarations #

def Disjoint {α : Type u_1} [inst : PartialOrder α] [inst : 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
theorem disjoint_comm {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} :
theorem Disjoint.symm {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] ⦃a : α ⦃b : α :
Disjoint a bDisjoint b a
theorem symmetric_disjoint {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] :
Symmetric Disjoint
@[simp]
theorem disjoint_bot_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
@[simp]
theorem disjoint_bot_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
theorem Disjoint.mono {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
Disjoint b dDisjoint a c
theorem Disjoint.mono_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} {c : α} (h : a b) :
Disjoint b cDisjoint a c
theorem Disjoint.mono_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} {c : α} :
b cDisjoint a cDisjoint a b
@[simp]
theorem disjoint_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
theorem Disjoint.eq_bot_of_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :
Disjoint a aa =

Alias of the forward direction of disjoint_self.

theorem Disjoint.ne {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (ha : a ) (hab : Disjoint a b) :
a b
theorem Disjoint.eq_bot_of_le {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (hab : Disjoint a b) (h : a b) :
a =
theorem Disjoint.eq_bot_of_ge {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (hab : Disjoint a b) :
b ab =
@[simp]
theorem disjoint_top {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :
@[simp]
theorem top_disjoint {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :
theorem disjoint_iff_inf_le {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :
theorem disjoint_iff {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :
Disjoint a b a b =
theorem Disjoint.le_bot {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :
Disjoint a ba b
theorem Disjoint.eq_bot {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :
Disjoint a ba b =
theorem disjoint_assoc {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} :
Disjoint (a b) c Disjoint a (b c)
theorem disjoint_left_comm {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} :
Disjoint a (b c) Disjoint b (a c)
theorem disjoint_right_comm {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} :
Disjoint (a b) c Disjoint (a c) b
theorem Disjoint.inf_left {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
Disjoint (a c) b
theorem Disjoint.inf_left' {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
Disjoint (c a) b
theorem Disjoint.inf_right {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
Disjoint a (b c)
theorem Disjoint.inf_right' {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :
Disjoint a (c b)
theorem Disjoint.of_disjoint_inf_of_le {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} (h : Disjoint (a b) c) (hle : a c) :
theorem Disjoint.of_disjoint_inf_of_le' {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} (h : Disjoint (a b) c) (hle : b c) :
@[simp]
theorem disjoint_sup_left {α : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] {a : α} {b : α} {c : α} :
@[simp]
theorem disjoint_sup_right {α : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] {a : α} {b : α} {c : α} :
theorem Disjoint.sup_left {α : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] {a : α} {b : α} {c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
Disjoint (a b) c
theorem Disjoint.sup_right {α : Type u_1} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : OrderBot α] {a : α} {b : α} {c : α} (h : a c b) (hd : Disjoint a c) :
a b
def Codisjoint {α : Type u_1} [inst : PartialOrder α] [inst : 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
theorem Codisjoint_comm {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} :
theorem Codisjoint.symm {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] ⦃a : α ⦃b : α :
theorem symmetric_codisjoint {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] :
Symmetric Codisjoint
@[simp]
theorem codisjoint_top_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
@[simp]
theorem codisjoint_top_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
theorem Codisjoint.mono {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} {c : α} {d : α} (h₁ : a b) (h₂ : c d) :
theorem Codisjoint.mono_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} {c : α} (h : a b) :
theorem Codisjoint.mono_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} {c : α} :
b cCodisjoint a bCodisjoint a c
@[simp]
theorem codisjoint_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
theorem Codisjoint.eq_top_of_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :
Codisjoint a aa =

Alias of the forward direction of codisjoint_self.

theorem Codisjoint.ne {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (ha : a ) (hab : Codisjoint a b) :
a b
theorem Codisjoint.eq_top_of_le {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) (h : b a) :
a =
theorem Codisjoint.eq_top_of_ge {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) :
a bb =
@[simp]
theorem codisjoint_bot {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :
@[simp]
theorem bot_codisjoint {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :
theorem codisjoint_iff_le_sup {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :
theorem codisjoint_iff {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :
theorem Codisjoint.top_le {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :
Codisjoint a b a b
theorem Codisjoint.eq_top {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :
Codisjoint a ba b =
theorem codisjoint_assoc {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} :
Codisjoint (a b) c Codisjoint a (b c)
theorem codisjoint_left_comm {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} :
Codisjoint a (b c) Codisjoint b (a c)
theorem codisjoint_right_comm {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} :
Codisjoint (a b) c Codisjoint (a c) b
theorem Codisjoint.sup_left {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
Codisjoint (a c) b
theorem Codisjoint.sup_left' {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
Codisjoint (c a) b
theorem Codisjoint.sup_right {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
Codisjoint a (b c)
theorem Codisjoint.sup_right' {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :
Codisjoint a (c b)
theorem Codisjoint.of_codisjoint_sup_of_le {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} (h : Codisjoint (a b) c) (hle : c a) :
theorem Codisjoint.of_codisjoint_sup_of_le' {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} (h : Codisjoint (a b) c) (hle : c b) :
@[simp]
theorem codisjoint_inf_left {α : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] {a : α} {b : α} {c : α} :
@[simp]
theorem codisjoint_inf_right {α : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] {a : α} {b : α} {c : α} :
theorem Codisjoint.inf_left {α : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] {a : α} {b : α} {c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) :
Codisjoint (a b) c
theorem Codisjoint.inf_right {α : Type u_1} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : OrderTop α] {a : α} {b : α} {c : α} (h : b a c) (hd : Codisjoint b c) :
a c
theorem Disjoint.dual {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :
Disjoint a bCodisjoint (OrderDual.toDual a) (OrderDual.toDual b)
theorem Codisjoint.dual {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :
Codisjoint a bDisjoint (OrderDual.toDual a) (OrderDual.toDual b)
@[simp]
theorem disjoint_toDual_iff {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :
Disjoint (OrderDual.toDual a) (OrderDual.toDual b) Codisjoint a b
@[simp]
theorem disjoint_ofDual_iff {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : αᵒᵈ} {b : αᵒᵈ} :
Disjoint (OrderDual.ofDual a) (OrderDual.ofDual b) Codisjoint a b
@[simp]
theorem codisjoint_toDual_iff {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :
Codisjoint (OrderDual.toDual a) (OrderDual.toDual b) Disjoint a b
@[simp]
theorem codisjoint_ofDual_iff {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : αᵒᵈ} {b : αᵒᵈ} :
Codisjoint (OrderDual.ofDual a) (OrderDual.ofDual b) Disjoint a b
theorem Disjoint.le_of_codisjoint {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {a : α} {b : α} {c : α} (hab : Disjoint a b) (hbc : Codisjoint b c) :
a c
structure IsCompl {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] (x : α) (y : α) :
  • If x and y are to be complementary in an order, they should be disjoint.

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

    Codisjoint : Codisjoint x y

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

Instances For
    theorem isCompl_iff {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} {b : α} :
    theorem IsCompl.symm {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
    theorem IsCompl.dual {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
    IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
    theorem IsCompl.ofDual {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : αᵒᵈ} {b : αᵒᵈ} (h : IsCompl a b) :
    IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b)
    theorem IsCompl.of_le {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h₁ : x y ) (h₂ : x y) :
    theorem IsCompl.of_eq {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h₁ : x y = ) (h₂ : x y = ) :
    theorem IsCompl.inf_eq_bot {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
    x y =
    theorem IsCompl.sup_eq_top {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :
    x y =
    theorem IsCompl.inf_left_le_of_le_sup_right {α : Type u_1} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
    x y = x z
    theorem IsCompl.inf_right_eq_bot_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
    x z = x y
    theorem IsCompl.disjoint_left_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
    Disjoint x y x z
    theorem IsCompl.disjoint_right_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :
    Disjoint x z x y
    theorem IsCompl.le_left_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
    z x Disjoint z y
    theorem IsCompl.le_right_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
    z y Disjoint z x
    theorem IsCompl.left_le_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
    theorem IsCompl.right_le_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :
    theorem IsCompl.Antitone {α : Type u_1} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (hxy : IsCompl x y) (hxz : IsCompl x z) :
    y = z
    theorem IsCompl.left_unique {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (hxz : IsCompl x z) (hyz : IsCompl y z) :
    x = y
    theorem IsCompl.sup_inf {α : Type u_1} [inst : DistribLattice α] [inst : 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} [inst : DistribLattice α] [inst : 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} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderBot α] [inst : OrderBot β] {x : α × β} {y : α × β} :
    Disjoint x y Disjoint x.fst y.fst Disjoint x.snd y.snd
    theorem Prod.codisjoint_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : OrderTop α] [inst : OrderTop β] {x : α × β} {y : α × β} :
    Codisjoint x y Codisjoint x.fst y.fst Codisjoint x.snd y.snd
    theorem Prod.isCompl_iff {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst : PartialOrder β] [inst : BoundedOrder α] [inst : BoundedOrder β] {x : α × β} {y : α × β} :
    IsCompl x y IsCompl x.fst y.fst IsCompl x.snd y.snd
    @[simp]
    theorem isCompl_toDual_iff {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {a : α} {b : α} :
    IsCompl (OrderDual.toDual a) (OrderDual.toDual b) IsCompl a b
    @[simp]
    theorem isCompl_ofDual_iff {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {a : αᵒᵈ} {b : αᵒᵈ} :
    IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b) IsCompl a b
    theorem isCompl_bot_top {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] :
    theorem isCompl_top_bot {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] :
    theorem eq_top_of_isCompl_bot {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl x ) :
    x =
    theorem eq_top_of_bot_isCompl {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl x) :
    x =
    theorem eq_bot_of_isCompl_top {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl x ) :
    x =
    theorem eq_bot_of_top_isCompl {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl x) :
    x =
    class ComplementedLattice (α : Type u_1) [inst : Lattice α] [inst : BoundedOrder α] :

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

    Instances
      Equations
      • One or more equations did not get rendered due to their size.