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.

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

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

source

ink

theorem disjoint_comm {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} :

Disjoint a b ↔ Disjoint b a

source

ink

theorem Disjoint.symm {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] ⦃a : α⦄ ⦃b : α⦄ :

Disjoint a b → Disjoint b a

source

ink

theorem symmetric_disjoint {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] :

Symmetric Disjoint

source

ink

@[simp]

theorem disjoint_bot_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

Disjoint ⊥ a

source

ink

@[simp]

theorem disjoint_bot_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

Disjoint a ⊥

source

ink

theorem Disjoint.mono {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} {c : α} {d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

Disjoint b d → Disjoint a c

source

ink

theorem Disjoint.mono_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} {c : α} (h : a ≤ b) :

Disjoint b c → Disjoint a c

source

ink

theorem Disjoint.mono_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} {c : α} :

b ≤ c → Disjoint a c → Disjoint a b

source

ink

@[simp]

theorem disjoint_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

Disjoint a a ↔ a = ⊥

source

ink

theorem Disjoint.eq_bot_of_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} :

Disjoint a a → a = ⊥

Alias of the forward direction of disjoint_self.

source

ink

theorem Disjoint.ne {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (ha : a ≠ ⊥) (hab : Disjoint a b) :

a ≠ b

source

ink

theorem Disjoint.eq_bot_of_le {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (hab : Disjoint a b) (h : a ≤ b) :

a = ⊥

source

ink

theorem Disjoint.eq_bot_of_ge {α : Type u_1} [inst : PartialOrder α] [inst : OrderBot α] {a : α} {b : α} (hab : Disjoint a b) :

b ≤ a → b = ⊥

source

ink

@[simp]

theorem disjoint_top {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :

Disjoint a ⊤ ↔ a = ⊥

source

ink

@[simp]

theorem top_disjoint {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :

Disjoint ⊤ a ↔ a = ⊥

source

ink

theorem disjoint_iff_inf_le {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :

Disjoint a b ↔ a ⊓ b ≤ ⊥

source

ink

theorem disjoint_iff {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :

Disjoint a b ↔ a ⊓ b = ⊥

source

ink

theorem Disjoint.le_bot {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :

Disjoint a b → a ⊓ b ≤ ⊥

source

ink

theorem Disjoint.eq_bot {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :

Disjoint a b → a ⊓ b = ⊥

source

ink

theorem disjoint_assoc {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} :

Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

source

ink

theorem disjoint_left_comm {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} :

Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

source

ink

theorem disjoint_right_comm {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} {c : α} :

Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

source

ink

theorem Disjoint.inf_left {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :

Disjoint (a ⊓ c) b

source

ink

theorem Disjoint.inf_left' {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :

Disjoint (c ⊓ a) b

source

ink

theorem Disjoint.inf_right {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :

Disjoint a (b ⊓ c)

source

ink

theorem Disjoint.inf_right' {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} (c : α) (h : Disjoint a b) :

Disjoint a (c ⊓ b)

source

ink

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) :

Disjoint a b

source

ink

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) :

Disjoint a b

source

ink

@[simp]

theorem disjoint_sup_left {α : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] {a : α} {b : α} {c : α} :

Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

source

ink

@[simp]

theorem disjoint_sup_right {α : Type u_1} [inst : DistribLattice α] [inst : OrderBot α] {a : α} {b : α} {c : α} :

Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

source

ink

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

source

ink

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)

source

ink

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

source

ink

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

source

ink

def Codisjoint {α : Type u_1} [inst : PartialOrder α] [inst : 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 implement Sup would require additional Decidable arguments.

Equations

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

source

ink

theorem Codisjoint_comm {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} :

Codisjoint a b ↔ Codisjoint b a

source

ink

theorem Codisjoint.symm {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] ⦃a : α⦄ ⦃b : α⦄ :

Codisjoint a b → Codisjoint b a

source

ink

theorem symmetric_codisjoint {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] :

Symmetric Codisjoint

source

ink

@[simp]

theorem codisjoint_top_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

Codisjoint ⊤ a

source

ink

@[simp]

theorem codisjoint_top_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

Codisjoint a ⊤

source

ink

theorem Codisjoint.mono {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} {c : α} {d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

Codisjoint a c → Codisjoint b d

source

ink

theorem Codisjoint.mono_left {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} {c : α} (h : a ≤ b) :

Codisjoint a c → Codisjoint b c

source

ink

theorem Codisjoint.mono_right {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} {c : α} :

b ≤ c → Codisjoint a b → Codisjoint a c

source

ink

@[simp]

theorem codisjoint_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

Codisjoint a a ↔ a = ⊤

source

ink

theorem Codisjoint.eq_top_of_self {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} :

Codisjoint a a → a = ⊤

Alias of the forward direction of codisjoint_self.

source

ink

theorem Codisjoint.ne {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (ha : a ≠ ⊤) (hab : Codisjoint a b) :

a ≠ b

source

ink

theorem Codisjoint.eq_top_of_le {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) (h : b ≤ a) :

a = ⊤

source

ink

theorem Codisjoint.eq_top_of_ge {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] {a : α} {b : α} (hab : Codisjoint a b) :

a ≤ b → b = ⊤

source

ink

@[simp]

theorem codisjoint_bot {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :

Codisjoint a ⊥ ↔ a = ⊤

source

ink

@[simp]

theorem bot_codisjoint {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} :

Codisjoint ⊥ a ↔ a = ⊤

source

ink

theorem codisjoint_iff_le_sup {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :

Codisjoint a b ↔ ⊤ ≤ a ⊔ b

source

ink

theorem codisjoint_iff {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :

Codisjoint a b ↔ a ⊔ b = ⊤

source

ink

theorem Codisjoint.top_le {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :

Codisjoint a b → ⊤ ≤ a ⊔ b

source

ink

theorem Codisjoint.eq_top {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :

Codisjoint a b → a ⊔ b = ⊤

source

ink

theorem codisjoint_assoc {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} :

Codisjoint (a ⊔ b) c ↔ Codisjoint a (b ⊔ c)

source

ink

theorem codisjoint_left_comm {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} :

Codisjoint a (b ⊔ c) ↔ Codisjoint b (a ⊔ c)

source

ink

theorem codisjoint_right_comm {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} {c : α} :

Codisjoint (a ⊔ b) c ↔ Codisjoint (a ⊔ c) b

source

ink

theorem Codisjoint.sup_left {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :

Codisjoint (a ⊔ c) b

source

ink

theorem Codisjoint.sup_left' {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :

Codisjoint (c ⊔ a) b

source

ink

theorem Codisjoint.sup_right {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :

Codisjoint a (b ⊔ c)

source

ink

theorem Codisjoint.sup_right' {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} (c : α) (h : Codisjoint a b) :

Codisjoint a (c ⊔ b)

source

ink

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) :

Codisjoint a b

source

ink

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) :

Codisjoint a b

source

ink

@[simp]

theorem codisjoint_inf_left {α : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] {a : α} {b : α} {c : α} :

Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c

source

ink

@[simp]

theorem codisjoint_inf_right {α : Type u_1} [inst : DistribLattice α] [inst : OrderTop α] {a : α} {b : α} {c : α} :

Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

source

ink

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

source

ink

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)

source

ink

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

source

ink

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

source

ink

theorem Disjoint.dual {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :

Disjoint a b → Codisjoint (↑OrderDual.toDual a) (↑OrderDual.toDual b)

source

ink

theorem Codisjoint.dual {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :

Codisjoint a b → Disjoint (↑OrderDual.toDual a) (↑OrderDual.toDual b)

source

ink

@[simp]

theorem disjoint_toDual_iff {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : α} {b : α} :

Disjoint (↑OrderDual.toDual a) (↑OrderDual.toDual b) ↔ Codisjoint a b

source

ink

@[simp]

theorem disjoint_ofDual_iff {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : αᵒᵈ} {b : αᵒᵈ} :

Disjoint (↑OrderDual.ofDual a) (↑OrderDual.ofDual b) ↔ Codisjoint a b

source

ink

@[simp]

theorem codisjoint_toDual_iff {α : Type u_1} [inst : SemilatticeInf α] [inst : OrderBot α] {a : α} {b : α} :

Codisjoint (↑OrderDual.toDual a) (↑OrderDual.toDual b) ↔ Disjoint a b

source

ink

@[simp]

theorem codisjoint_ofDual_iff {α : Type u_1} [inst : SemilatticeSup α] [inst : OrderTop α] {a : αᵒᵈ} {b : αᵒᵈ} :

Codisjoint (↑OrderDual.ofDual a) (↑OrderDual.ofDual b) ↔ Disjoint a b

source

ink

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

source

ink

structure IsCompl {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] (x : α) (y : α) :

Prop

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

source

ink

theorem isCompl_iff {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : α} {b : α} :

IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b

source

ink

theorem IsCompl.symm {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :

IsCompl y x

source

ink

theorem IsCompl.dual {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :

IsCompl (↑OrderDual.toDual x) (↑OrderDual.toDual y)

source

ink

theorem IsCompl.ofDual {α : Type u_1} [inst : PartialOrder α] [inst : BoundedOrder α] {a : αᵒᵈ} {b : αᵒᵈ} (h : IsCompl a b) :

IsCompl (↑OrderDual.ofDual a) (↑OrderDual.ofDual b)

source

ink

theorem IsCompl.of_le {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h₁ : x ⊓ y ≤ ⊥) (h₂ : ⊤ ≤ x ⊔ y) :

IsCompl x y

source

ink

theorem IsCompl.of_eq {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h₁ : x ⊓ y = ⊥) (h₂ : x ⊔ y = ⊤) :

IsCompl x y

source

ink

theorem IsCompl.inf_eq_bot {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :

x ⊓ y = ⊥

source

ink

theorem IsCompl.sup_eq_top {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} {y : α} (h : IsCompl x y) :

x ⊔ y = ⊤

source

ink

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

source

ink

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

source

ink

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

source

ink

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

source

ink

theorem IsCompl.disjoint_left_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :

Disjoint x y ↔ x ≤ z

source

ink

theorem IsCompl.disjoint_right_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl y z) :

Disjoint x z ↔ x ≤ y

source

ink

theorem IsCompl.le_left_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :

z ≤ x ↔ Disjoint z y

source

ink

theorem IsCompl.le_right_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :

z ≤ y ↔ Disjoint z x

source

ink

theorem IsCompl.left_le_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :

x ≤ z ↔ Codisjoint z y

source

ink

theorem IsCompl.right_le_iff {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (h : IsCompl x y) :

y ≤ z ↔ Codisjoint z x

source

ink

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

source

ink

theorem IsCompl.right_unique {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (hxy : IsCompl x y) (hxz : IsCompl x z) :

y = z

source

ink

theorem IsCompl.left_unique {α : Type u_1} [inst : DistribLattice α] [inst : BoundedOrder α] {x : α} {y : α} {z : α} (hxz : IsCompl x z) (hyz : IsCompl y z) :

x = y

source

ink

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')

source

ink

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')

source

ink

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

source

ink

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

source

ink

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

source

ink

@[simp]

theorem isCompl_toDual_iff {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {a : α} {b : α} :

IsCompl (↑OrderDual.toDual a) (↑OrderDual.toDual b) ↔ IsCompl a b

source

ink

@[simp]

theorem isCompl_ofDual_iff {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {a : αᵒᵈ} {b : αᵒᵈ} :

IsCompl (↑OrderDual.ofDual a) (↑OrderDual.ofDual b) ↔ IsCompl a b

source

ink

theorem isCompl_bot_top {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] :

IsCompl ⊥ ⊤

source

ink

theorem isCompl_top_bot {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] :

IsCompl ⊤ ⊥

source

ink

theorem eq_top_of_isCompl_bot {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl x ⊥) :

x = ⊤

source

ink

theorem eq_top_of_bot_isCompl {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl ⊥ x) :

x = ⊤

source

ink

theorem eq_bot_of_isCompl_top {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl x ⊤) :

x = ⊥

source

ink

theorem eq_bot_of_top_isCompl {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] {x : α} (h : IsCompl ⊤ x) :

x = ⊥

source

ink

class ComplementedLattice (α : Type u_1) [inst : Lattice α] [inst : BoundedOrder α] :

Prop

In a ComplementedLattice, every element admits a complement.
exists_isCompl : ∀ (a : α), ∃ b, IsCompl a b

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

Instances

source

ink

instance ComplementedLattice.instComplementedLatticeOrderDualLatticeBoundedOrderToLEToPreorderToPartialOrderToSemilatticeInf {α : Type u_1} [inst : Lattice α] [inst : BoundedOrder α] [inst : ComplementedLattice α] :

ComplementedLattice αᵒᵈ

Equations

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