(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 ≤ max a b

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Alias of the reverse direction of sup_eq_left.

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

Alias of the forward direction of sup_eq_left.

theorem le_of_sup_eq {α : Type u} [SemilatticeSup α] {a b : α} : max 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 → max 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 → min 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 → min a b = a

Alias of the reverse direction of inf_eq_left.

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

Alias of the forward direction of inf_eq_right.

theorem le_of_inf_eq {α : Type u} [SemilatticeInf α] {a b : α} : min 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) : max a c ≤ max b d

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem inf_inf_distrib_right {α : Type u} [SemilatticeInf α] (a b c : α) : min (min a b) c = min (min a c) (min 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

theorem inf_le_sup {α : Type u} [Lattice α] {a b : α} : min a b ≤ max a b

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

@[simp]

theorem inf_left_le_sup_right {α : Type u} [Lattice α] {a b c : α} : min a b ≤ max b c

@[simp]

theorem inf_right_le_sup_left {α : Type u} [Lattice α] {a b c : α} : min b c ≤ max a b

@[simp]

theorem inf_right_le_sup_right {α : Type u} [Lattice α] {a b c : α} : min b a ≤ max b c

@[simp]

theorem inf_left_le_sup_left {α : Type u} [Lattice α] {a b c : α} : min a b ≤ max c b

Distributivity laws

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

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

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

theorem sup_inf_self {α : Type u} [Lattice α] {a b : α} : max a (min a b) = a

theorem sup_eq_iff_inf_eq {α : Type u} [Lattice α] {a b : α} : max a b = b ↔ min a b = a

theorem inf_eq_iff_sup_eq {α : Type u} [Lattice α] {a b : α} : min a b = b ↔ max 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 : α) : min (max x y) (max x z) ≤ max x (min y z)

  The infimum distributes over the supremum

@[reducible, inline]

abbrev DistribLattice.ofInfSupLe {α : Type u} [Lattice α] (inf_sup_le : ∀ (a b c : α), min a (max b c) ≤ max (min a b) (min 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 : α} : min (max x y) (max x z) ≤ max x (min y z)

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

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

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

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

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

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

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