# Disjointness and complements #

This file defines `Disjoint`, `Codisjoint`, and the `IsCompl` 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.
- `IsCompl 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.
- `ComplementedLattice α`: Typeclass stating that any element of a lattice has a complement.

source
def Disjoint {α : Type u_1} [PartialOrder α] [OrderBot α] (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 `Inf` would require additional `Decidable` arguments.

Equations

- Disjoint a b = ∀ ⦃x : α⦄, x ≤ a → x ≤ b → x ≤ ⊥

Instances For

source
@[simp]
theorem disjoint_of_subsingleton {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} [Subsingleton α] :
Disjoint a b
source
theorem disjoint_comm {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} :
Disjoint a b ↔ Disjoint b a
source
theorem Disjoint.symm {α : Type u_1} [PartialOrder α] [OrderBot α] ⦃a b : α⦄ :
Disjoint a b → Disjoint b a
source
theorem symmetric_disjoint {α : Type u_1} [PartialOrder α] [OrderBot α] :
Symmetric Disjoint
source
@[simp]
theorem disjoint_bot_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
Disjoint ⊥ a
source
@[simp]
theorem disjoint_bot_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
Disjoint a ⊥
source
theorem Disjoint.mono {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
Disjoint b d → Disjoint a c
source
theorem Disjoint.mono_left {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} (h : a ≤ b) :
Disjoint b c → Disjoint a c
source
theorem Disjoint.mono_right {α : Type u_1} [PartialOrder α] [OrderBot α] {a b c : α} (h : b ≤ c) :
Disjoint a c → Disjoint a b
source
@[simp]
theorem disjoint_self {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
Disjoint a a ↔ a = ⊥
source
theorem Disjoint.eq_bot_of_self {α : Type u_1} [PartialOrder α] [OrderBot α] {a : α} :
Disjoint a a → a = ⊥

Alias of the forward direction of `disjoint_self`.

source
theorem Disjoint.ne {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (ha : a ≠ ⊥) (hab : Disjoint a b) :
a ≠ b
source
theorem Disjoint.eq_bot_of_le {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) (h : a ≤ b) :
a = ⊥
source
theorem Disjoint.eq_bot_of_ge {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) :
b ≤ a → b = ⊥
source
theorem Disjoint.eq_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) :
a = b ↔ a = ⊥ ∧ b = ⊥
source
theorem Disjoint.ne_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (hab : Disjoint a b) :
a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥
source
theorem disjoint_of_le_iff_left_eq_bot {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} (h : a ≤ b) :
Disjoint a b ↔ a = ⊥
source
@[simp]
theorem disjoint_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
Disjoint a ⊤ ↔ a = ⊥
source
@[simp]
theorem top_disjoint {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
Disjoint ⊤ a ↔ a = ⊥
source
theorem disjoint_iff_inf_le {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
Disjoint a b ↔ a ⊓ b ≤ ⊥
source
theorem disjoint_iff {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
Disjoint a b ↔ a ⊓ b = ⊥
source
theorem Disjoint.le_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
Disjoint a b → a ⊓ b ≤ ⊥
source
theorem Disjoint.eq_bot {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} :
Disjoint a b → a ⊓ b = ⊥
source
theorem disjoint_assoc {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} :
Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)
source
theorem disjoint_left_comm {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} :
Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)
source
theorem disjoint_right_comm {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} :
Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b
source
theorem Disjoint.inf_left {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
Disjoint (a ⊓ c) b
source
theorem Disjoint.inf_left' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
Disjoint (c ⊓ a) b
source
theorem Disjoint.inf_right {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
Disjoint a (b ⊓ c)
source
theorem Disjoint.inf_right' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b : α} (c : α) (h : Disjoint a b) :
Disjoint a (c ⊓ b)
source
theorem Disjoint.of_disjoint_inf_of_le {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} (h : Disjoint (a ⊓ b) c) (hle : a ≤ c) :
Disjoint a b
source
theorem Disjoint.of_disjoint_inf_of_le' {α : Type u_1} [SemilatticeInf α] [OrderBot α] {a b c : α} (h : Disjoint (a ⊓ b) c) (hle : b ≤ c) :
Disjoint a b
source
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
source
@[simp]
theorem disjoint_sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} :
Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c
source
@[simp]
theorem disjoint_sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} :
Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c
source
theorem Disjoint.sup_left {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
Disjoint (a ⊔ b) c
source
theorem Disjoint.sup_right {α : Type u_1} [DistribLattice α] [OrderBot α] {a b c : α} (hb : Disjoint a b) (hc : Disjoint a c) :
Disjoint a (b ⊔ c)
source
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
source
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
source
def Codisjoint {α : Type u_1} [PartialOrder α] [OrderTop α] (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 implementing `Sup` would require additional `Decidable` arguments.

Equations

- Codisjoint a b = ∀ ⦃x : α⦄, a ≤ x → b ≤ x → ⊤ ≤ x

Instances For

source
theorem codisjoint_comm {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} :
Codisjoint a b ↔ Codisjoint b a
source
theorem Codisjoint.symm {α : Type u_1} [PartialOrder α] [OrderTop α] ⦃a b : α⦄ :
Codisjoint a b → Codisjoint b a
source
theorem symmetric_codisjoint {α : Type u_1} [PartialOrder α] [OrderTop α] :
Symmetric Codisjoint
source
@[simp]
theorem codisjoint_top_left {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
Codisjoint ⊤ a
source
@[simp]
theorem codisjoint_top_right {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
Codisjoint a ⊤
source
theorem Codisjoint.mono {α : Type u_1} [PartialOrder α] [OrderTop α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
Codisjoint a c → Codisjoint b d
source
theorem Codisjoint.mono_left {α : Type u_1} [PartialOrder α] [OrderTop α] {a b c : α} (h : a ≤ b) :
Codisjoint a c → Codisjoint b c
source
theorem Codisjoint.mono_right {α : Type u_1} [PartialOrder α] [OrderTop α] {a b c : α} :
b ≤ c → Codisjoint a b → Codisjoint a c
source
@[simp]
theorem codisjoint_self {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
Codisjoint a a ↔ a = ⊤
source
theorem Codisjoint.eq_top_of_self {α : Type u_1} [PartialOrder α] [OrderTop α] {a : α} :
Codisjoint a a → a = ⊤

Alias of the forward direction of `codisjoint_self`.

source
theorem Codisjoint.ne {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (ha : a ≠ ⊤) (hab : Codisjoint a b) :
a ≠ b
source
theorem Codisjoint.eq_top_of_le {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) (h : b ≤ a) :
a = ⊤
source
theorem Codisjoint.eq_top_of_ge {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) :
a ≤ b → b = ⊤
source
theorem Codisjoint.eq_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) :
a = b ↔ a = ⊤ ∧ b = ⊤
source
theorem Codisjoint.ne_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} (hab : Codisjoint a b) :
a ≠ b ↔ a ≠ ⊤ ∨ b ≠ ⊤
source
@[simp]
theorem codisjoint_bot {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
Codisjoint a ⊥ ↔ a = ⊤
source
@[simp]
theorem bot_codisjoint {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a : α} :
Codisjoint ⊥ a ↔ a = ⊤
source
theorem Codisjoint.ne_bot_of_ne_top {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α} (h : Codisjoint a b) (ha : a ≠ ⊤) :
b ≠ ⊥
source
@[deprecated Codisjoint.ne_bot_of_ne_top (since := "2025-11-07")]
theorem Codisjoint.ne_bot_of_ne_top' {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α} (h : Codisjoint a b) (hb : b ≠ ⊤) :
a ≠ ⊥
source
theorem codisjoint_iff_le_sup {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
Codisjoint a b ↔ ⊤ ≤ a ⊔ b
source
theorem codisjoint_iff {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
Codisjoint a b ↔ a ⊔ b = ⊤
source
theorem Codisjoint.top_le {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
Codisjoint a b → ⊤ ≤ a ⊔ b
source
theorem Codisjoint.eq_top {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} :
Codisjoint a b → a ⊔ b = ⊤
source
theorem codisjoint_assoc {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} :
Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c)
source
theorem codisjoint_left_comm {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} :
Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)
source
theorem codisjoint_right_comm {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} :
Codisjoint (a ⊔ b) c ↔ Codisjoint (a ⊔ c) b
source
theorem Codisjoint.sup_left {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
Codisjoint (a ⊔ c) b
source
theorem Codisjoint.sup_left' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
Codisjoint (c ⊔ a) b
source
theorem Codisjoint.sup_right {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
Codisjoint a (b ⊔ c)
source
theorem Codisjoint.sup_right' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b : α} (c : α) (h : Codisjoint a b) :
Codisjoint a (c ⊔ b)
source
theorem Codisjoint.of_codisjoint_sup_of_le {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} (h : Codisjoint (a ⊔ b) c) (hle : c ≤ a) :
Codisjoint a b
source
theorem Codisjoint.of_codisjoint_sup_of_le' {α : Type u_1} [SemilatticeSup α] [OrderTop α] {a b c : α} (h : Codisjoint (a ⊔ b) c) (hle : c ≤ b) :
Codisjoint a b
source
@[simp]
theorem codisjoint_inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} :
Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c
source
@[simp]
theorem codisjoint_inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} :
Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c
source
theorem Codisjoint.inf_left {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} (ha : Codisjoint a c) (hb : Codisjoint b c) :
Codisjoint (a ⊓ b) c
source
theorem Codisjoint.inf_right {α : Type u_1} [DistribLattice α] [OrderTop α] {a b c : α} (hb : Codisjoint a b) (hc : Codisjoint a c) :
Codisjoint a (b ⊓ c)
source
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
source
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
source
theorem Disjoint.dual {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} :
Disjoint a b → Codisjoint (OrderDual.toDual a) (OrderDual.toDual b)
source
theorem Codisjoint.dual {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} :
Codisjoint a b → Disjoint (OrderDual.toDual a) (OrderDual.toDual b)
source
@[simp]
theorem disjoint_toDual_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α} :
Disjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Codisjoint a b
source
@[simp]
theorem disjoint_ofDual_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α ᵒᵈ} :
Disjoint (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ Codisjoint a b
source
@[simp]
theorem codisjoint_toDual_iff {α : Type u_1} [PartialOrder α] [OrderBot α] {a b : α} :
Codisjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Disjoint a b
source
@[simp]
theorem codisjoint_ofDual_iff {α : Type u_1} [PartialOrder α] [OrderTop α] {a b : α ᵒᵈ} :
Codisjoint (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ Disjoint a b
source
theorem Disjoint.le_of_codisjoint {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b c : α} (hab : Disjoint a b) (hbc : Codisjoint b c) :
a ≤ c
source
structure IsCompl {α : Type u_1} [PartialOrder α] [BoundedOrder α] (x y : α) :
Prop

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

source
theorem isCompl_iff {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α} :
IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b
source
theorem IsCompl.symm {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x y : α} (h : IsCompl x y) :
IsCompl y x
source
theorem isCompl_comm {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x y : α} :
IsCompl x y ↔ IsCompl y x
source
theorem IsCompl.dual {α : Type u_1} [PartialOrder α] [BoundedOrder α] {x y : α} (h : IsCompl x y) :
IsCompl (OrderDual.toDual x) (OrderDual.toDual y)
source
theorem IsCompl.ofDual {α : Type u_1} [PartialOrder α] [BoundedOrder α] {a b : α ᵒᵈ} (h : IsCompl a b) :
IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b)
source
theorem IsCompl.of_le {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) :
IsCompl x y
source
theorem IsCompl.of_eq {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) :
IsCompl x y
source
theorem IsCompl.inf_eq_bot {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h : IsCompl x y) :
x ⊓ y = ⊥
source
theorem IsCompl.sup_eq_top {α : Type u_1} [Lattice α] [BoundedOrder α] {x y : α} (h : IsCompl x y) :
x ⊔ y = ⊤
source
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
source
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
source
theorem IsCompl.inf_left_eq_bot_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) :
x ⊓ y = ⊥ ↔ x ≤ z
source
theorem IsCompl.inf_right_eq_bot_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) :
x ⊓ z = ⊥ ↔ x ≤ y
source
theorem IsCompl.disjoint_left_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) :
Disjoint x y ↔ x ≤ z
source
theorem IsCompl.disjoint_right_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl y z) :
Disjoint x z ↔ x ≤ y
source
theorem IsCompl.le_left_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl x y) :
z ≤ x ↔ Disjoint z y
source
theorem IsCompl.le_right_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl x y) :
z ≤ y ↔ Disjoint z x
source
theorem IsCompl.left_le_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl x y) :
x ≤ z ↔ Codisjoint z y
source
theorem IsCompl.right_le_iff {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (h : IsCompl x y) :
y ≤ z ↔ Codisjoint z x
source
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
source
theorem IsCompl.right_unique {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (hxy : IsCompl x y) (hxz : IsCompl x z) :
y = z
source
theorem IsCompl.left_unique {α : Type u_1} [DistribLattice α] [BoundedOrder α] {x y z : α} (hxz : IsCompl x z) (hyz : IsCompl y z) :
x = y
source
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')
source
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')
source
theorem Prod.disjoint_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderBot α] [OrderBot β] {x y : α × β} :
Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
source
theorem Prod.codisjoint_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [OrderTop α] [OrderTop β] {x y : α × β} :
Codisjoint x y ↔ Codisjoint x.fst y.fst ∧ Codisjoint x.snd y.snd
source
theorem Prod.isCompl_iff {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] [BoundedOrder α] [BoundedOrder β] {x y : α × β} :
IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd
source
@[simp]
theorem isCompl_toDual_iff {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α} :
IsCompl (OrderDual.toDual a) (OrderDual.toDual b) ↔ IsCompl a b
source
@[simp]
theorem isCompl_ofDual_iff {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : α ᵒᵈ} :
IsCompl (OrderDual.ofDual a) (OrderDual.ofDual b) ↔ IsCompl a b
source
theorem isCompl_bot_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
IsCompl ⊥ ⊤
source
theorem isCompl_top_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
IsCompl ⊤ ⊥
source
theorem eq_top_of_isCompl_bot {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x ⊥) :
x = ⊤
source
theorem eq_top_of_bot_isCompl {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl ⊥ x) :
x = ⊤
source
theorem eq_bot_of_isCompl_top {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl x ⊤) :
x = ⊥
source
theorem eq_bot_of_top_isCompl {α : Type u_1} [Lattice α] [BoundedOrder α] {x : α} (h : IsCompl ⊤ x) :
x = ⊥
source
def IsComplemented {α : Type u_1} [Lattice α] [BoundedOrder α] (a : α) :
Prop

An element is complemented if it has a complement.

Equations

- IsComplemented a = ∃ (b : α), IsCompl a b

Instances For

source
theorem isComplemented_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
IsComplemented ⊥
source
theorem isComplemented_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
IsComplemented ⊤
source
theorem IsComplemented.sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : α} :
IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b)
source
theorem IsComplemented.inf {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : α} :
IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b)
source
class ComplementedLattice (α : Type u_2) [Lattice α] [BoundedOrder α] :
Prop

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

- exists_isCompl (a : α) : ∃ (b : α), IsCompl a b

  In a `ComplementedLattice`, every element admits a complement.

Instances

source
theorem complementedLattice_iff (α : Type u_2) [Lattice α] [BoundedOrder α] :
ComplementedLattice α ↔ ∀ (a : α), ∃ (b : α), IsCompl a b
source
theorem Subsingleton.instComplementedLattice {α : Type u_1} [Lattice α] [BoundedOrder α] [Subsingleton α] :
ComplementedLattice α
source
instance ComplementedLattice.instOrderDual {α : Type u_1} [Lattice α] [BoundedOrder α] [ComplementedLattice α] :
ComplementedLattice α ᵒᵈ
source
@[reducible, inline]
abbrev Complementeds (α : Type u_2) [Lattice α] [BoundedOrder α] :
Type u_2

The sublattice of complemented elements.

Equations

- Complementeds α = { a : α // IsComplemented a }

Instances For

source
instance Complementeds.hasCoeT {α : Type u_1} [Lattice α] [BoundedOrder α] :
CoeTC (Complementeds α) α
Equations

- Complementeds.hasCoeT = { coe := Subtype.val }

source
theorem Complementeds.coe_injective {α : Type u_1} [Lattice α] [BoundedOrder α] :
Function.Injective Subtype.val
source
@[simp]
theorem Complementeds.coe_inj {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : Complementeds α} :
↑a = ↑b ↔ a = b
source
theorem Complementeds.coe_le_coe {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : Complementeds α} :
↑a ≤ ↑b ↔ a ≤ b
source
theorem Complementeds.coe_lt_coe {α : Type u_1} [Lattice α] [BoundedOrder α] {a b : Complementeds α} :
↑a < ↑b ↔ a < b
source
instance Complementeds.instBoundedOrder {α : Type u_1} [Lattice α] [BoundedOrder α] :
BoundedOrder (Complementeds α)
Equations

- Complementeds.instBoundedOrder = Subtype.boundedOrder ⋯ ⋯

source
@[simp]
theorem Complementeds.coe_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
↑⊥ = ⊥
source
@[simp]
theorem Complementeds.coe_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
↑⊤ = ⊤
source
theorem Complementeds.mk_bot {α : Type u_1} [Lattice α] [BoundedOrder α] :
⟨⊥, ⋯⟩ = ⊥
source
theorem Complementeds.mk_top {α : Type u_1} [Lattice α] [BoundedOrder α] :
⟨⊤, ⋯⟩ = ⊤
source
instance Complementeds.instInhabited {α : Type u_1} [Lattice α] [BoundedOrder α] :
Inhabited (Complementeds α)
Equations

- Complementeds.instInhabited = { default := ⊥ }

source
instance Complementeds.instMax {α : Type u_1} [DistribLattice α] [BoundedOrder α] :
Max (Complementeds α)
Equations

- Complementeds.instMax = { max := fun (a b : Complementeds α) => ⟨↑a ⊔ ↑b, ⋯⟩ }

source
instance Complementeds.instMin {α : Type u_1} [DistribLattice α] [BoundedOrder α] :
Min (Complementeds α)
Equations

- Complementeds.instMin = { min := fun (a b : Complementeds α) => ⟨↑a ⊓ ↑b, ⋯⟩ }

source
@[simp]
theorem Complementeds.coe_sup {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a b : Complementeds α) :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[simp]
theorem Complementeds.coe_inf {α : Type u_1} [DistribLattice α] [BoundedOrder α] (a b : Complementeds α) :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
@[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, ⋯⟩
source
@[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, ⋯⟩
source
instance Complementeds.instDistribLattice {α : Type u_1} [DistribLattice α] [BoundedOrder α] :
DistribLattice (Complementeds α)
Equations

- Complementeds.instDistribLattice = Function.Injective.distribLattice Subtype.val ⋯ ⋯ ⋯

source
@[simp]
theorem Complementeds.disjoint_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : Complementeds α} :
Disjoint ↑a ↑b ↔ Disjoint a b
source
@[simp]
theorem Complementeds.codisjoint_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : Complementeds α} :
Codisjoint ↑a ↑b ↔ Codisjoint a b
source
@[simp]
theorem Complementeds.isCompl_coe {α : Type u_1} [DistribLattice α] [BoundedOrder α] {a b : Complementeds α} :
IsCompl ↑a ↑b ↔ IsCompl a b
source
instance Complementeds.instComplementedLattice {α : Type u_1} [DistribLattice α] [BoundedOrder α] :
ComplementedLattice (Complementeds α)