(Semi-)lattices

Semilattices are partially ordered sets with join (least upper bound, or sup) or meet (greatest lower bound, or inf) operations. Lattices are posets that are both join-semilattices and meet-semilattices.

Distributive lattices are lattices which satisfy any of four equivalent distributivity properties, of sup over inf, on the left or on the right.

Main declarations

• SemilatticeSup: a type class for join semilattices
• SemilatticeInf: a type class for meet semilattices
• Lattice: a type class for lattices
• DistribLattice: a type class for distributive lattices.

Notation

• a ⊔ b: the supremum or join of a and b
• a ⊓ b: the infimum or meet of a and b

Tags

semilattice, lattice

Semilattices

class SemilatticeSup (α : Type u) extends PartialOrder α : Type u

A SemilatticeSup is a join-semilattice, that is, a partial order with a join (a.k.a. lub / least upper bound, sup / supremum) operation ⊔ which is the least element larger than both factors.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α

  The binary supremum, used to derive Max α

• le_sup_left (a b : α) : a ≤ sup a b

  The supremum is an upper bound on the first argument

• le_sup_right (a b : α) : b ≤ sup a b

  The supremum is an upper bound on the second argument

• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c

  The supremum is the least upper bound

class SemilatticeInf (α : Type u) extends PartialOrder α : Type u

A SemilatticeInf is a meet-semilattice, that is, a partial order with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation ⊓ which is the greatest element smaller than both factors.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• inf : α → α → α

  The binary infimum, used to derive Min α

• inf_le_left (a b : α) : inf a b ≤ a

  The infimum is a lower bound on the first argument

• inf_le_right (a b : α) : inf a b ≤ b

  The infimum is a lower bound on the second argument

• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ inf b c

  The infimum is the greatest lower bound

@[instance_reducible]

instance SemilatticeSup.toMax {α : Type u} [SemilatticeSup α] : Max α

Equations

• SemilatticeSup.toMax = { max := fun (a b : α) => SemilatticeSup.sup a b }

@[instance_reducible]

instance SemilatticeInf.toMin {α : Type u} [SemilatticeInf α] : Min α

Equations

• SemilatticeInf.toMin = { min := fun (a b : α) => SemilatticeInf.inf a b }

@[simp]

theorem le_sup_left {α : Type u} [SemilatticeSup α] {a b : α} : a ≤ a ⊔ b

@[simp]

theorem inf_le_left {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b ≤ a

@[simp]

theorem le_sup_right {α : Type u} [SemilatticeSup α] {a b : α} : b ≤ a ⊔ b

@[simp]

theorem inf_le_right {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b ≤ b

theorem sup_le {α : Type u} [SemilatticeSup α] {a b c : α} : a ≤ c → b ≤ c → a ⊔ b ≤ c

theorem le_inf {α : Type u} [SemilatticeInf α] {c a b : α} : c ≤ a → c ≤ b → c ≤ a ⊓ b

theorem le_sup_of_le_left {α : Type u} [SemilatticeSup α] {a b c : α} (h : c ≤ a) : c ≤ a ⊔ b

theorem inf_le_of_left_le {α : Type u} [SemilatticeInf α] {a b c : α} (h : a ≤ c) : a ⊓ b ≤ c

theorem le_sup_of_le_right {α : Type u} [SemilatticeSup α] {a b c : α} (h : c ≤ b) : c ≤ a ⊔ b

theorem inf_le_of_right_le {α : Type u} [SemilatticeInf α] {a b c : α} (h : b ≤ c) : a ⊓ b ≤ c

theorem lt_sup_of_lt_left {α : Type u} [SemilatticeSup α] {a b c : α} (h : c < a) : c < a ⊔ b

theorem inf_lt_of_left_lt {α : Type u} [SemilatticeInf α] {a b c : α} (h : a < c) : a ⊓ b < c

theorem lt_sup_of_lt_right {α : Type u} [SemilatticeSup α] {a b c : α} (h : c < b) : c < a ⊔ b

theorem inf_lt_of_right_lt {α : Type u} [SemilatticeInf α] {a b c : α} (h : b < c) : a ⊓ b < c

@[simp]

theorem sup_le_iff {α : Type u} [SemilatticeSup α] {a b c : α} : a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c

@[simp]

theorem le_inf_iff {α : Type u} [SemilatticeInf α] {c a b : α} : c ≤ a ⊓ b ↔ c ≤ a ∧ c ≤ b

@[simp]

theorem sup_eq_left {α : Type u} [SemilatticeSup α] {a b : α} : a ⊔ b = a ↔ b ≤ a

@[simp]

theorem inf_eq_left {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b = a ↔ a ≤ b

@[simp]

theorem sup_eq_right {α : Type u} [SemilatticeSup α] {a b : α} : a ⊔ b = b ↔ a ≤ b

@[simp]

theorem inf_eq_right {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b = b ↔ b ≤ a

@[simp]

theorem left_eq_sup {α : Type u} [SemilatticeSup α] {a b : α} : a = a ⊔ b ↔ b ≤ a

@[simp]

theorem left_eq_inf {α : Type u} [SemilatticeInf α] {a b : α} : a = a ⊓ b ↔ a ≤ b

@[simp]

theorem right_eq_sup {α : Type u} [SemilatticeSup α] {a b : α} : b = a ⊔ b ↔ a ≤ b

@[simp]

theorem right_eq_inf {α : Type u} [SemilatticeInf α] {a b : α} : b = a ⊓ b ↔ b ≤ a

theorem le_of_sup_eq' {α : Type u} [SemilatticeSup α] {a b : α} : a ⊔ b = a → b ≤ a

Alias of the forward direction of sup_eq_left.

@[simp]

theorem sup_of_le_left {α : Type u} [SemilatticeSup α] {a b : α} : b ≤ a → a ⊔ b = a

Alias of the reverse direction of sup_eq_left.

theorem le_of_sup_eq {α : Type u} [SemilatticeSup α] {a b : α} : a ⊔ b = b → a ≤ b

Alias of the forward direction of sup_eq_right.

@[simp]

theorem sup_of_le_right {α : Type u} [SemilatticeSup α] {a b : α} : a ≤ b → a ⊔ b = b

Alias of the reverse direction of sup_eq_right.

@[simp]

theorem inf_of_le_right {α : Type u} [SemilatticeInf α] {a b : α} : b ≤ a → a ⊓ b = b

Alias of the reverse direction of inf_eq_right.

@[simp]

theorem inf_of_le_left {α : Type u} [SemilatticeInf α] {a b : α} : a ≤ b → a ⊓ b = a

Alias of the reverse direction of inf_eq_left.

theorem le_of_inf_eq' {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b = b → b ≤ a

Alias of the forward direction of inf_eq_right.

theorem le_of_inf_eq {α : Type u} [SemilatticeInf α] {a b : α} : a ⊓ b = a → a ≤ b

Alias of the forward direction of inf_eq_left.

theorem sup_le_sup {α : Type u} [SemilatticeSup α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d

theorem inf_le_inf {α : Type u} [SemilatticeInf α] {a b c d : α} (h₁ : b ≤ a) (h₂ : d ≤ c) : b ⊓ d ≤ a ⊓ c

theorem sup_le_sup_left {α : Type u} [SemilatticeSup α] {a b : α} (h₁ : a ≤ b) (c : α) : c ⊔ a ≤ c ⊔ b

theorem inf_le_inf_left {α : Type u} [SemilatticeInf α] {a b : α} (c : α) (h₁ : b ≤ a) : c ⊓ b ≤ c ⊓ a

theorem sup_le_sup_right {α : Type u} [SemilatticeSup α] {a b : α} (h₁ : a ≤ b) (c : α) : a ⊔ c ≤ b ⊔ c

theorem inf_le_inf_right {α : Type u} [SemilatticeInf α] {a b : α} (c : α) (h₁ : b ≤ a) : b ⊓ c ≤ a ⊓ c

theorem sup_idem {α : Type u} [SemilatticeSup α] (a : α) : a ⊔ a = a

theorem inf_idem {α : Type u} [SemilatticeInf α] (a : α) : a ⊓ a = a

instance instIdempotentOpMax_mathlib {α : Type u} [SemilatticeSup α] : Std.IdempotentOp fun (x1 x2 : α) => x1 ⊔ x2

instance instIdempotentOpMin_mathlib {α : Type u} [SemilatticeInf α] : Std.IdempotentOp fun (x1 x2 : α) => x1 ⊓ x2

theorem sup_comm {α : Type u} [SemilatticeSup α] (a b : α) : a ⊔ b = b ⊔ a

theorem inf_comm {α : Type u} [SemilatticeInf α] (a b : α) : a ⊓ b = b ⊓ a

instance instCommutativeMax_mathlib {α : Type u} [SemilatticeSup α] : Std.Commutative fun (x1 x2 : α) => x1 ⊔ x2

instance instCommutativeMin_mathlib {α : Type u} [SemilatticeInf α] : Std.Commutative fun (x1 x2 : α) => x1 ⊓ x2

theorem sup_assoc {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

theorem inf_assoc {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

instance instAssociativeMax_mathlib {α : Type u} [SemilatticeSup α] : Std.Associative fun (x1 x2 : α) => x1 ⊔ x2

instance instAssociativeMin_mathlib {α : Type u} [SemilatticeInf α] : Std.Associative fun (x1 x2 : α) => x1 ⊓ x2

theorem sup_left_right_swap {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ b ⊔ c = c ⊔ b ⊔ a

theorem inf_left_right_swap {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ b ⊓ c = c ⊓ b ⊓ a

theorem sup_left_idem {α : Type u} [SemilatticeSup α] (a b : α) : a ⊔ (a ⊔ b) = a ⊔ b

theorem inf_left_idem {α : Type u} [SemilatticeInf α] (a b : α) : a ⊓ (a ⊓ b) = a ⊓ b

theorem sup_right_idem {α : Type u} [SemilatticeSup α] (a b : α) : a ⊔ b ⊔ b = a ⊔ b

theorem inf_right_idem {α : Type u} [SemilatticeInf α] (a b : α) : a ⊓ b ⊓ b = a ⊓ b

theorem sup_left_comm {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

theorem inf_left_comm {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)

theorem sup_right_comm {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ b

theorem inf_right_comm {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b

theorem sup_sup_sup_comm {α : Type u} [SemilatticeSup α] (a b c d : α) : a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

theorem inf_inf_inf_comm {α : Type u} [SemilatticeInf α] (a b c d : α) : a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)

theorem sup_rotate {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ b ⊔ c = b ⊔ c ⊔ a

theorem inf_rotate {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ b ⊓ c = b ⊓ c ⊓ a

theorem sup_rotate' {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ (b ⊔ c) = b ⊔ (c ⊔ a)

theorem inf_rotate' {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (c ⊓ a)

theorem sup_sup_distrib_left {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

theorem inf_inf_distrib_left {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c)

theorem sup_sup_distrib_right {α : Type u} [SemilatticeSup α] (a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

theorem inf_inf_distrib_right {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ (b ⊓ c)

Lattices

class Lattice (α : Type u) extends SemilatticeSup α, SemilatticeInf α : Type u

A lattice is a join-semilattice which is also a meet-semilattice.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c

@[instance_reducible]

def Lattice.mkDual {α : Type u_1} [SemilatticeInf α] (sup : α → α → α) (le_sup_left : ∀ (a b : α), a ≤ sup a b) (le_sup_right : ∀ (a b : α), b ≤ sup a b) (sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c) : Lattice α

Auxiliary constructor for to_dual.

Equations

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

theorem inf_le_sup {α : Type u} [Lattice α] {a b : α} : a ⊓ b ≤ a ⊔ b

theorem sup_le_inf {α : Type u} [Lattice α] {a b : α} : a ⊔ b ≤ a ⊓ b ↔ a = b

@[simp]

theorem inf_left_le_sup_right {α : Type u} [Lattice α] {a b c : α} : a ⊓ b ≤ b ⊔ c

@[simp]

theorem inf_right_le_sup_left {α : Type u} [Lattice α] {a b c : α} : b ⊓ c ≤ a ⊔ b

@[simp]

theorem inf_right_le_sup_right {α : Type u} [Lattice α] {a b c : α} : b ⊓ a ≤ b ⊔ c

@[simp]

theorem inf_left_le_sup_left {α : Type u} [Lattice α] {a b c : α} : a ⊓ b ≤ c ⊔ b

Distributivity laws

theorem sup_inf_le {α : Type u} [Lattice α] {a b c : α} : a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c)

theorem le_inf_sup {α : Type u} [Lattice α] {a b c : α} : a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c)

theorem inf_sup_self {α : Type u} [Lattice α] {a b : α} : a ⊓ (a ⊔ b) = a

theorem sup_inf_self {α : Type u} [Lattice α] {a b : α} : a ⊔ a ⊓ b = a

theorem sup_eq_iff_inf_eq {α : Type u} [Lattice α] {a b : α} : a ⊔ b = b ↔ a ⊓ b = a

theorem inf_eq_iff_sup_eq {α : Type u} [Lattice α] {a b : α} : a ⊓ b = b ↔ a ⊔ b = a

Distributive lattices

class DistribLattice (α : Type u_1) extends Lattice α : Type u_1

A distributive lattice is a lattice that satisfies any of four equivalent distributive properties (of sup over inf or inf over sup, on the left or right).

The definition here chooses le_sup_inf: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z). To prove distributivity from the dual law, use DistribLattice.ofInfSupLe.

A classic example of a distributive lattice is the lattice of subsets of a set, and in fact this example is generic in the sense that every distributive lattice is realizable as a sublattice of a powerset lattice.

• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• le_sup_inf (x y z : α) : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

  The infimum distributes over the supremum

@[reducible, inline]

abbrev DistribLattice.ofInfSupLe {α : Type u} [Lattice α] (inf_sup_le : ∀ (a b c : α), a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) : DistribLattice α

Prove distributivity of an existing lattice from the dual distributive law.

Equations

• DistribLattice.ofInfSupLe inf_sup_le = { toLattice := inst✝, le_sup_inf := ⋯ }

theorem le_sup_inf {α : Type u} [DistribLattice α] {x y z : α} : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

theorem sup_inf_left {α : Type u} [DistribLattice α] (a b c : α) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

theorem sup_inf_right {α : Type u} [DistribLattice α] (a b c : α) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

theorem inf_sup_left {α : Type u} [DistribLattice α] (a b c : α) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c

theorem inf_sup_le {α : Type u} [DistribLattice α] {x y z : α} : x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z

theorem inf_sup_right {α : Type u} [DistribLattice α] (a b c : α) : (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

theorem le_of_inf_le_sup_le {α : Type u} [DistribLattice α] {x y z : α} (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y

theorem eq_of_inf_eq_sup_eq {α : Type u} [DistribLattice α] {a b c : α} (h₁ : b ⊓ a = c ⊓ a) (h₂ : b ⊔ a = c ⊔ a) : b = c