order.disjoint

# Disjointness and complements #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines disjoint, codisjoint, and the is_compl predicate.

## Main declarations #

• disjoint x y: two elements of a lattice are disjoint if their inf is the bottom element.
• codisjoint x y: two elements of a lattice are codisjoint if their join is the top element.
• is_compl x y: In a bounded lattice, predicate for "x is a complement of y". Note that in a non distributive lattice, an element can have several complements.
• complemented_lattice α: Typeclass stating that any element of a lattice has a complement.
def disjoint {α : Type u_1} [order_bot α] (a b : α) :
Prop

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 has_inf would require additional decidable arguments.

Equations
Instances for disjoint
theorem disjoint.comm {α : Type u_1} [order_bot α] {a b : α} :
b a
@[symm]
theorem disjoint.symm {α : Type u_1} [order_bot α] ⦃a b : α⦄ :
b a
theorem symmetric_disjoint {α : Type u_1} [order_bot α] :
@[simp]
theorem disjoint_bot_left {α : Type u_1} [order_bot α] {a : α} :
@[simp]
theorem disjoint_bot_right {α : Type u_1} [order_bot α] {a : α} :
theorem disjoint.mono {α : Type u_1} [order_bot α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
d c
theorem disjoint.mono_left {α : Type u_1} [order_bot α] {a b c : α} (h : a b) :
c c
theorem disjoint.mono_right {α : Type u_1} [order_bot α] {a b c : α} :
b c c b
@[simp]
theorem disjoint_self {α : Type u_1} [order_bot α] {a : α} :
a a =
theorem disjoint.eq_bot_of_self {α : Type u_1} [order_bot α] {a : α} :
a a =

Alias of the forward direction of disjoint_self.

theorem disjoint.ne {α : Type u_1} [order_bot α] {a b : α} (ha : a ) (hab : b) :
a b
theorem disjoint.eq_bot_of_le {α : Type u_1} [order_bot α] {a b : α} (hab : b) (h : a b) :
a =
theorem disjoint.eq_bot_of_ge {α : Type u_1} [order_bot α] {a b : α} (hab : b) :
b a b =
@[simp]
theorem disjoint_top {α : Type u_1} {a : α} :
a =
@[simp]
theorem top_disjoint {α : Type u_1} {a : α} :
a =
theorem disjoint_iff_inf_le {α : Type u_1} [order_bot α] {a b : α} :
b a b
theorem disjoint_iff {α : Type u_1} [order_bot α] {a b : α} :
b a b =
theorem disjoint.le_bot {α : Type u_1} [order_bot α] {a b : α} :
b a b
theorem disjoint.eq_bot {α : Type u_1} [order_bot α] {a b : α} :
b a b =
theorem disjoint_assoc {α : Type u_1} [order_bot α] {a b c : α} :
disjoint (a b) c (b c)
theorem disjoint_left_comm {α : Type u_1} [order_bot α] {a b c : α} :
(b c) (a c)
theorem disjoint_right_comm {α : Type u_1} [order_bot α] {a b c : α} :
disjoint (a b) c disjoint (a c) b
theorem disjoint.inf_left {α : Type u_1} [order_bot α] {a b : α} (c : α) (h : b) :
disjoint (a c) b
theorem disjoint.inf_left' {α : Type u_1} [order_bot α] {a b : α} (c : α) (h : b) :
disjoint (c a) b
theorem disjoint.inf_right {α : Type u_1} [order_bot α] {a b : α} (c : α) (h : b) :
(b c)
theorem disjoint.inf_right' {α : Type u_1} [order_bot α] {a b : α} (c : α) (h : b) :
(c b)
theorem disjoint.of_disjoint_inf_of_le {α : Type u_1} [order_bot α] {a b c : α} (h : disjoint (a b) c) (hle : a c) :
b
theorem disjoint.of_disjoint_inf_of_le' {α : Type u_1} [order_bot α] {a b c : α} (h : disjoint (a b) c) (hle : b c) :
b
@[simp]
theorem disjoint_sup_left {α : Type u_1} [order_bot α] {a b c : α} :
disjoint (a b) c c c
@[simp]
theorem disjoint_sup_right {α : Type u_1} [order_bot α] {a b c : α} :
(b c) b c
theorem disjoint.sup_left {α : Type u_1} [order_bot α] {a b c : α} (ha : c) (hb : c) :
disjoint (a b) c
theorem disjoint.sup_right {α : Type u_1} [order_bot α] {a b c : α} (hb : b) (hc : c) :
(b c)
theorem disjoint.left_le_of_le_sup_right {α : Type u_1} [order_bot α] {a b c : α} (h : a b c) (hd : c) :
a b
theorem disjoint.left_le_of_le_sup_left {α : Type u_1} [order_bot α] {a b c : α} (h : a c b) (hd : c) :
a b
def codisjoint {α : Type u_1} [order_top α] (a b : α) :
Prop

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 has_sup would require additional decidable arguments.

Equations
Instances for codisjoint
theorem codisjoint.comm {α : Type u_1} [order_top α] {a b : α} :
b a
@[symm]
theorem codisjoint.symm {α : Type u_1} [order_top α] ⦃a b : α⦄ :
b a
theorem symmetric_codisjoint {α : Type u_1} [order_top α] :
@[simp]
theorem codisjoint_top_left {α : Type u_1} [order_top α] {a : α} :
@[simp]
theorem codisjoint_top_right {α : Type u_1} [order_top α] {a : α} :
theorem codisjoint.mono {α : Type u_1} [order_top α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
c d
theorem codisjoint.mono_left {α : Type u_1} [order_top α] {a b c : α} (h : a b) :
c c
theorem codisjoint.mono_right {α : Type u_1} [order_top α] {a b c : α} :
b c b c
@[simp]
theorem codisjoint_self {α : Type u_1} [order_top α] {a : α} :
a a =
theorem codisjoint.eq_top_of_self {α : Type u_1} [order_top α] {a : α} :
a a =

Alias of the forward direction of codisjoint_self.

theorem codisjoint.ne {α : Type u_1} [order_top α] {a b : α} (ha : a ) (hab : b) :
a b
theorem codisjoint.eq_top_of_le {α : Type u_1} [order_top α] {a b : α} (hab : b) (h : b a) :
a =
theorem codisjoint.eq_top_of_ge {α : Type u_1} [order_top α] {a b : α} (hab : b) :
a b b =
@[simp]
theorem codisjoint_bot {α : Type u_1} {a : α} :
a =
@[simp]
theorem bot_codisjoint {α : Type u_1} {a : α} :
a =
theorem codisjoint_iff_le_sup {α : Type u_1} [order_top α] {a b : α} :
b a b
theorem codisjoint_iff {α : Type u_1} [order_top α] {a b : α} :
b a b =
theorem codisjoint.top_le {α : Type u_1} [order_top α] {a b : α} :
b a b
theorem codisjoint.eq_top {α : Type u_1} [order_top α] {a b : α} :
b a b =
theorem codisjoint_assoc {α : Type u_1} [order_top α] {a b c : α} :
codisjoint (a b) c (b c)
theorem codisjoint_left_comm {α : Type u_1} [order_top α] {a b c : α} :
(b c) (a c)
theorem codisjoint_right_comm {α : Type u_1} [order_top α] {a b c : α} :
codisjoint (a b) c codisjoint (a c) b
theorem codisjoint.sup_left {α : Type u_1} [order_top α] {a b : α} (c : α) (h : b) :
codisjoint (a c) b
theorem codisjoint.sup_left' {α : Type u_1} [order_top α] {a b : α} (c : α) (h : b) :
codisjoint (c a) b
theorem codisjoint.sup_right {α : Type u_1} [order_top α] {a b : α} (c : α) (h : b) :
(b c)
theorem codisjoint.sup_right' {α : Type u_1} [order_top α] {a b : α} (c : α) (h : b) :
(c b)
theorem codisjoint.of_codisjoint_sup_of_le {α : Type u_1} [order_top α] {a b c : α} (h : codisjoint (a b) c) (hle : c a) :
b
theorem codisjoint.of_codisjoint_sup_of_le' {α : Type u_1} [order_top α] {a b c : α} (h : codisjoint (a b) c) (hle : c b) :
b
@[simp]
theorem codisjoint_inf_left {α : Type u_1} [order_top α] {a b c : α} :
codisjoint (a b) c c c
@[simp]
theorem codisjoint_inf_right {α : Type u_1} [order_top α] {a b c : α} :
(b c) b c
theorem codisjoint.inf_left {α : Type u_1} [order_top α] {a b c : α} (ha : c) (hb : c) :
codisjoint (a b) c
theorem codisjoint.inf_right {α : Type u_1} [order_top α] {a b c : α} (hb : b) (hc : c) :
(b c)
theorem codisjoint.left_le_of_le_inf_right {α : Type u_1} [order_top α] {a b c : α} (h : a b c) (hd : c) :
a c
theorem codisjoint.left_le_of_le_inf_left {α : Type u_1} [order_top α] {a b c : α} (h : b a c) (hd : c) :
a c
theorem disjoint.dual {α : Type u_1} [order_bot α] {a b : α} :
theorem codisjoint.dual {α : Type u_1} [order_top α] {a b : α} :
@[simp]
theorem disjoint_to_dual_iff {α : Type u_1} [order_top α] {a b : α} :
@[simp]
theorem disjoint_of_dual_iff {α : Type u_1} [order_bot α] {a b : αᵒᵈ} :
@[simp]
theorem codisjoint_to_dual_iff {α : Type u_1} [order_bot α] {a b : α} :
@[simp]
theorem codisjoint_of_dual_iff {α : Type u_1} [order_top α] {a b : αᵒᵈ} :
theorem disjoint.le_of_codisjoint {α : Type u_1} {a b c : α} (hab : b) (hbc : c) :
a c
structure is_compl {α : Type u_1} (x y : α) :
Prop
• disjoint : y
• codisjoint : y

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

Instances for is_compl
theorem is_compl_iff {α : Type u_1} {a b : α} :
b b b
@[protected, symm]
theorem is_compl.symm {α : Type u_1} {x y : α} (h : y) :
x
theorem is_compl.dual {α : Type u_1} {x y : α} (h : y) :
theorem is_compl.of_dual {α : Type u_1} {a b : αᵒᵈ} (h : b) :
theorem is_compl.of_le {α : Type u_1} [lattice α] {x y : α} (h₁ : x y ) (h₂ : x y) :
y
theorem is_compl.of_eq {α : Type u_1} [lattice α] {x y : α} (h₁ : x y = ) (h₂ : x y = ) :
y
theorem is_compl.inf_eq_bot {α : Type u_1} [lattice α] {x y : α} (h : y) :
x y =
theorem is_compl.sup_eq_top {α : Type u_1} [lattice α] {x y : α} (h : y) :
x y =
theorem is_compl.inf_left_le_of_le_sup_right {α : Type u_1} {a b x y : α} (h : y) (hle : a b y) :
a x b
theorem is_compl.le_sup_right_iff_inf_left_le {α : Type u_1} {x y a b : α} (h : y) :
a b y a x b
theorem is_compl.inf_left_eq_bot_iff {α : Type u_1} {x y z : α} (h : z) :
x y = x z
theorem is_compl.inf_right_eq_bot_iff {α : Type u_1} {x y z : α} (h : z) :
x z = x y
theorem is_compl.disjoint_left_iff {α : Type u_1} {x y z : α} (h : z) :
y x z
theorem is_compl.disjoint_right_iff {α : Type u_1} {x y z : α} (h : z) :
z x y
theorem is_compl.le_left_iff {α : Type u_1} {x y z : α} (h : y) :
z x y
theorem is_compl.le_right_iff {α : Type u_1} {x y z : α} (h : y) :
z y x
theorem is_compl.left_le_iff {α : Type u_1} {x y z : α} (h : y) :
x z y
theorem is_compl.right_le_iff {α : Type u_1} {x y z : α} (h : y) :
y z x
@[protected]
theorem is_compl.antitone {α : Type u_1} {x y x' y' : α} (h : y) (h' : is_compl x' y') (hx : x x') :
y' y
theorem is_compl.right_unique {α : Type u_1} {x y z : α} (hxy : y) (hxz : z) :
y = z
theorem is_compl.left_unique {α : Type u_1} {x y z : α} (hxz : z) (hyz : z) :
x = y
theorem is_compl.sup_inf {α : Type u_1} {x y x' y' : α} (h : y) (h' : is_compl x' y') :
is_compl (x x') (y y')
theorem is_compl.inf_sup {α : Type u_1} {x y x' y' : α} (h : y) (h' : is_compl x' y') :
is_compl (x x') (y y')
@[protected]
theorem prod.disjoint_iff {α : Type u_1} {β : Type u_2} [order_bot α] [order_bot β] {x y : α × β} :
y y.fst y.snd
@[protected]
theorem prod.codisjoint_iff {α : Type u_1} {β : Type u_2} [order_top α] [order_top β] {x y : α × β} :
y y.fst y.snd
@[protected]
theorem prod.is_compl_iff {α : Type u_1} {β : Type u_2} {x y : α × β} :
y y.fst y.snd
@[simp]
theorem is_compl_to_dual_iff {α : Type u_1} [lattice α] {a b : α} :
b
@[simp]
theorem is_compl_of_dual_iff {α : Type u_1} [lattice α] {a b : αᵒᵈ} :
b
theorem is_compl_bot_top {α : Type u_1} [lattice α]  :
theorem is_compl_top_bot {α : Type u_1} [lattice α]  :
theorem eq_top_of_is_compl_bot {α : Type u_1} [lattice α] {x : α} (h : ) :
x =
theorem eq_top_of_bot_is_compl {α : Type u_1} [lattice α] {x : α} (h : x) :
x =
theorem eq_bot_of_is_compl_top {α : Type u_1} [lattice α] {x : α} (h : ) :
x =
theorem eq_bot_of_top_is_compl {α : Type u_1} [lattice α] {x : α} (h : x) :
x =
def is_complemented {α : Type u_1} [lattice α] (a : α) :
Prop

An element is complemented if it has a complement.

Equations
theorem is_complemented_bot {α : Type u_1} [lattice α]  :
theorem is_complemented_top {α : Type u_1} [lattice α]  :
theorem is_complemented.sup {α : Type u_1} {a b : α} :
theorem is_complemented.inf {α : Type u_1} {a b : α} :
@[class]
structure complemented_lattice (α : Type u_2) [lattice α]  :
Prop
• exists_is_compl : (a : α),

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

Instances of this typeclass
@[protected, instance]
@[protected, instance]
def complementeds.partial_order (α : Type u_1) [lattice α]  :
@[reducible]
def complementeds (α : Type u_1) [lattice α]  :
Type u_1

The sublattice of complemented elements.

Equations
• = {a //
@[protected, instance]
def complementeds.has_coe_t {α : Type u_1} [lattice α]  :
α
Equations
theorem complementeds.coe_injective {α : Type u_1} [lattice α]  :
@[simp, norm_cast]
theorem complementeds.coe_inj {α : Type u_1} [lattice α] {a b : complementeds α} :
a = b a = b
@[simp, norm_cast]
theorem complementeds.coe_le_coe {α : Type u_1} [lattice α] {a b : complementeds α} :
a b a b
@[simp, norm_cast]
theorem complementeds.coe_lt_coe {α : Type u_1} [lattice α] {a b : complementeds α} :
a < b a < b
@[protected, instance]
def complementeds.bounded_order {α : Type u_1} [lattice α]  :
Equations
@[simp, norm_cast]
theorem complementeds.coe_bot {α : Type u_1} [lattice α]  :
@[simp, norm_cast]
theorem complementeds.coe_top {α : Type u_1} [lattice α]  :
@[simp]
theorem complementeds.mk_bot {α : Type u_1} [lattice α]  :
, _⟩ =
@[simp]
theorem complementeds.mk_top {α : Type u_1} [lattice α]  :
, _⟩ =
@[protected, instance]
def complementeds.inhabited {α : Type u_1} [lattice α]  :
Equations
@[protected, instance]
def complementeds.has_sup {α : Type u_1}  :
Equations
@[protected, instance]
def complementeds.has_inf {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem complementeds.coe_sup {α : Type u_1} (a b : complementeds α) :
(a b) = a b
@[simp, norm_cast]
theorem complementeds.coe_inf {α : Type u_1} (a b : complementeds α) :
(a b) = a b
@[simp]
theorem complementeds.mk_sup_mk {α : Type u_1} {a b : α} (ha : is_complemented a) (hb : is_complemented b) :
a, ha⟩ b, hb⟩ = a b, _⟩
@[simp]
theorem complementeds.mk_inf_mk {α : Type u_1} {a b : α} (ha : is_complemented a) (hb : is_complemented b) :
a, ha⟩ b, hb⟩ = a b, _⟩
@[protected, instance]
def complementeds.distrib_lattice {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem complementeds.disjoint_coe {α : Type u_1} {a b : complementeds α} :
b b
@[simp, norm_cast]
theorem complementeds.codisjoint_coe {α : Type u_1} {a b : complementeds α} :
b b
@[simp, norm_cast]
theorem complementeds.is_compl_coe {α : Type u_1} {a b : complementeds α} :
b b
@[protected, instance]