mathlib documentation

order.lattice

(Semi-)lattices #

Semilattices are partially ordered sets with join (greatest lower bound, or sup) or meet (least upper 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 #

Notations #

TODO #

Tags #

semilattice, lattice

theorem le_antisymm' {α : Type u} [partial_order α] {a b : α} :
(:a b:)b aa = b

Join-semilattices #

@[class]
structure semilattice_sup (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c

A semilattice_sup 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.

Instances
@[instance]
def semilattice_sup.to_has_sup (α : Type u) [self : semilattice_sup α] :
@[instance]
def semilattice_sup.to_partial_order (α : Type u) [self : semilattice_sup α] :
def semilattice_sup.mk' {α : Type u_1} [has_sup α] (sup_comm : ∀ (a b : α), a b = b a) (sup_assoc : ∀ (a b c : α), a b c = a (b c)) (sup_idem : ∀ (a : α), a a = a) :

A type with a commutative, associative and idempotent binary sup operation has the structure of a join-semilattice.

The partial order is defined so that a ≤ b unfolds to a ⊔ b = b; cf. sup_eq_right.

Equations
@[instance]
def order_dual.has_sup (α : Type u_1) [has_inf α] :
Equations
@[instance]
def order_dual.has_inf (α : Type u_1) [has_sup α] :
Equations
@[simp]
theorem le_sup_left {α : Type u} [semilattice_sup α] {a b : α} :
a a b
theorem le_sup_left' {α : Type u} [semilattice_sup α] {a b : α} :
a (:a b:)
@[simp]
theorem le_sup_right {α : Type u} [semilattice_sup α] {a b : α} :
b a b
theorem le_sup_right' {α : Type u} [semilattice_sup α] {a b : α} :
b (:a b:)
theorem le_sup_of_le_left {α : Type u} [semilattice_sup α] {a b c : α} (h : c a) :
c a b
theorem le_sup_of_le_right {α : Type u} [semilattice_sup α] {a b c : α} (h : c b) :
c a b
theorem sup_le {α : Type u} [semilattice_sup α] {a b c : α} :
a cb ca b c
@[simp]
theorem sup_le_iff {α : Type u} [semilattice_sup α] {a b c : α} :
a b c a c b c
@[simp]
theorem sup_eq_left {α : Type u} [semilattice_sup α] {a b : α} :
a b = a b a
theorem sup_of_le_left {α : Type u} [semilattice_sup α] {a b : α} (h : b a) :
a b = a
@[simp]
theorem left_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
a = a b b a
@[simp]
theorem sup_eq_right {α : Type u} [semilattice_sup α] {a b : α} :
a b = b a b
theorem sup_of_le_right {α : Type u} [semilattice_sup α] {a b : α} (h : a b) :
a b = b
@[simp]
theorem right_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
b = a b a b
theorem sup_le_sup {α : Type u} [semilattice_sup α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
a c b d
theorem sup_le_sup_left {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a b) (c : α) :
c a c b
theorem sup_le_sup_right {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a b) (c : α) :
a c b c
theorem le_of_sup_eq {α : Type u} [semilattice_sup α] {a b : α} (h : a b = b) :
a b
theorem sup_ind {α : Type u} [semilattice_sup α] [is_total α has_le.le] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) :
p (a b)
@[simp]
theorem sup_lt_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
b c < a b < a c < a
@[simp]
theorem le_sup_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
a b c a b a c
@[simp]
theorem lt_sup_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
a < b c a < b a < c
@[simp]
theorem sup_idem {α : Type u} [semilattice_sup α] {a : α} :
a a = a
@[instance]
theorem sup_comm {α : Type u} [semilattice_sup α] {a b : α} :
a b = b a
@[instance]
theorem sup_assoc {α : Type u} [semilattice_sup α] {a b c : α} :
a b c = a (b c)
@[instance]
theorem sup_left_right_swap {α : Type u} [semilattice_sup α] (a b c : α) :
a b c = c b a
@[simp]
theorem sup_left_idem {α : Type u} [semilattice_sup α] {a b : α} :
a (a b) = a b
@[simp]
theorem sup_right_idem {α : Type u} [semilattice_sup α] {a b : α} :
a b b = a b
theorem sup_left_comm {α : Type u} [semilattice_sup α] (a b c : α) :
a (b c) = b (a c)
theorem sup_right_comm {α : Type u} [semilattice_sup α] (a b c : α) :
a b c = a c b
theorem forall_le_or_exists_lt_sup {α : Type u} [semilattice_sup α] (a : α) :
(∀ (b : α), b a) ∃ (b : α), a < b
theorem monotone.forall_le_of_antitone {α : Type u} [semilattice_sup α] {β : Type u_1} [preorder β] {f g : α → β} (hf : monotone f) (hg : antitone g) (h : f g) (m n : α) :
f m g n

If f is monotone, g is antitone, and f ≤ g, then for all a, b we have f a ≤ g b.

theorem semilattice_sup.ext_sup {α : Type u_1} {A B : semilattice_sup α} (H : ∀ (x y : α), x y x y) (x y : α) :
x y = x y
theorem semilattice_sup.ext {α : Type u_1} {A B : semilattice_sup α} (H : ∀ (x y : α), x y x y) :
A = B

Meet-semilattices #

@[instance]
def semilattice_inf.to_has_inf (α : Type u) [self : semilattice_inf α] :
@[class]
structure semilattice_inf (α : Type u) :
Type u
  • inf : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c

A semilattice_inf 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.

Instances
@[instance]
def semilattice_inf.to_partial_order (α : Type u) [self : semilattice_inf α] :
@[simp]
theorem inf_le_left {α : Type u} [semilattice_inf α] {a b : α} :
a b a
theorem inf_le_left' {α : Type u} [semilattice_inf α] {a b : α} :
(:a b:) a
@[simp]
theorem inf_le_right {α : Type u} [semilattice_inf α] {a b : α} :
a b b
theorem inf_le_right' {α : Type u} [semilattice_inf α] {a b : α} :
(:a b:) b
theorem le_inf {α : Type u} [semilattice_inf α] {a b c : α} :
a ba ca b c
theorem inf_le_of_left_le {α : Type u} [semilattice_inf α] {a b c : α} (h : a c) :
a b c
theorem inf_le_of_right_le {α : Type u} [semilattice_inf α] {a b c : α} (h : b c) :
a b c
@[simp]
theorem le_inf_iff {α : Type u} [semilattice_inf α] {a b c : α} :
a b c a b a c
@[simp]
theorem inf_eq_left {α : Type u} [semilattice_inf α] {a b : α} :
a b = a a b
theorem inf_of_le_left {α : Type u} [semilattice_inf α] {a b : α} (h : a b) :
a b = a
@[simp]
theorem left_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
a = a b a b
@[simp]
theorem inf_eq_right {α : Type u} [semilattice_inf α] {a b : α} :
a b = b b a
theorem inf_of_le_right {α : Type u} [semilattice_inf α] {a b : α} (h : b a) :
a b = b
@[simp]
theorem right_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
b = a b b a
theorem inf_le_inf {α : Type u} [semilattice_inf α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
a c b d
theorem inf_le_inf_right {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b c) :
b a c a
theorem inf_le_inf_left {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b c) :
a b a c
theorem le_of_inf_eq {α : Type u} [semilattice_inf α] {a b : α} (h : a b = a) :
a b
theorem inf_ind {α : Type u} [semilattice_inf α] [is_total α has_le.le] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) :
p (a b)
@[simp]
theorem lt_inf_iff {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b c : α} :
a < b c a < b a < c
@[simp]
theorem inf_le_iff {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b c : α} :
b c a b a c a
@[simp]
theorem inf_idem {α : Type u} [semilattice_inf α] {a : α} :
a a = a
@[instance]
theorem inf_comm {α : Type u} [semilattice_inf α] {a b : α} :
a b = b a
@[instance]
theorem inf_assoc {α : Type u} [semilattice_inf α] {a b c : α} :
a b c = a (b c)
@[instance]
theorem inf_left_right_swap {α : Type u} [semilattice_inf α] (a b c : α) :
a b c = c b a
@[simp]
theorem inf_left_idem {α : Type u} [semilattice_inf α] {a b : α} :
a (a b) = a b
@[simp]
theorem inf_right_idem {α : Type u} [semilattice_inf α] {a b : α} :
a b b = a b
theorem inf_left_comm {α : Type u} [semilattice_inf α] (a b c : α) :
a (b c) = b (a c)
theorem inf_right_comm {α : Type u} [semilattice_inf α] (a b c : α) :
a b c = a c b
theorem forall_le_or_exists_lt_inf {α : Type u} [semilattice_inf α] (a : α) :
(∀ (b : α), a b) ∃ (b : α), b < a
theorem semilattice_inf.ext_inf {α : Type u_1} {A B : semilattice_inf α} (H : ∀ (x y : α), x y x y) (x y : α) :
x y = x y
theorem semilattice_inf.ext {α : Type u_1} {A B : semilattice_inf α} (H : ∀ (x y : α), x y x y) :
A = B
def semilattice_inf.mk' {α : Type u_1} [has_inf α] (inf_comm : ∀ (a b : α), a b = b a) (inf_assoc : ∀ (a b c : α), a b c = a (b c)) (inf_idem : ∀ (a : α), a a = a) :

A type with a commutative, associative and idempotent binary inf operation has the structure of a meet-semilattice.

The partial order is defined so that a ≤ b unfolds to b ⊓ a = a; cf. inf_eq_right.

Equations

Lattices #

@[instance]
def lattice.to_semilattice_inf (α : Type u) [self : lattice α] :
@[instance]
def lattice.to_semilattice_sup (α : Type u) [self : lattice α] :
@[class]
structure lattice (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c

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

Instances
theorem semilattice_sup_mk'_partial_order_eq_semilattice_inf_mk'_partial_order {α : Type u_1} [has_sup α] [has_inf α] (sup_comm : ∀ (a b : α), a b = b a) (sup_assoc : ∀ (a b c : α), a b c = a (b c)) (sup_idem : ∀ (a : α), a a = a) (inf_comm : ∀ (a b : α), a b = b a) (inf_assoc : ∀ (a b c : α), a b c = a (b c)) (inf_idem : ∀ (a : α), a a = a) (sup_inf_self : ∀ (a b : α), a a b = a) (inf_sup_self : ∀ (a b : α), a (a b) = a) :

The partial orders from semilattice_sup_mk' and semilattice_inf_mk' agree if sup and inf satisfy the lattice absorption laws sup_inf_self (a ⊔ a ⊓ b = a) and inf_sup_self (a ⊓ (a ⊔ b) = a).

def lattice.mk' {α : Type u_1} [has_sup α] [has_inf α] (sup_comm : ∀ (a b : α), a b = b a) (sup_assoc : ∀ (a b c : α), a b c = a (b c)) (inf_comm : ∀ (a b : α), a b = b a) (inf_assoc : ∀ (a b c : α), a b c = a (b c)) (sup_inf_self : ∀ (a b : α), a a b = a) (inf_sup_self : ∀ (a b : α), a (a b) = a) :

A type with a pair of commutative and associative binary operations which satisfy two absorption laws relating the two operations has the structure of a lattice.

The partial order is defined so that a ≤ b unfolds to a ⊔ b = b; cf. sup_eq_right.

Equations

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 lattice.ext {α : Type u_1} {A B : lattice α} (H : ∀ (x y : α), x y x y) :
A = B

Distributive lattices #

@[instance]
def distrib_lattice.to_lattice (α : Type u_1) [self : distrib_lattice α] :
@[class]
structure distrib_lattice (α : Type u_1) :
Type u_1
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c : α), a bb ca c
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_sup_left : ∀ (a b : α), a a b
  • le_sup_right : ∀ (a b : α), b a b
  • sup_le : ∀ (a b c : α), a cb ca b c
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c : α), a ba ca b c
  • le_sup_inf : ∀ (x y z : α), (x y) (x z) x y z

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

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.

Instances
theorem le_sup_inf {α : Type u} [distrib_lattice α] {x y z : α} :
(x y) (x z) x y z
theorem sup_inf_left {α : Type u} [distrib_lattice α] {x y z : α} :
x y z = (x y) (x z)
theorem sup_inf_right {α : Type u} [distrib_lattice α] {x y z : α} :
y z x = (y x) (z x)
theorem inf_sup_left {α : Type u} [distrib_lattice α] {x y z : α} :
x (y z) = x y x z
theorem inf_sup_right {α : Type u} [distrib_lattice α] {x y z : α} :
(y z) x = y x z x
theorem le_of_inf_le_sup_le {α : Type u} [distrib_lattice α] {x y z : α} (h₁ : x z y z) (h₂ : x z y z) :
x y
theorem eq_of_inf_eq_sup_eq {α : Type u} [distrib_lattice α] {a b c : α} (h₁ : b a = c a) (h₂ : b a = c a) :
b = c

Lattices derived from linear orders #

@[instance]
def lattice_of_linear_order {α : Type u} [o : linear_order α] :
Equations
theorem sup_eq_max {α : Type u} [linear_order α] {x y : α} :
x y = max x y
theorem inf_eq_min {α : Type u} [linear_order α] {x y : α} :
x y = min x y
def lattice.to_linear_order (α : Type u) [lattice α] [decidable_eq α] [decidable_rel has_le.le] [decidable_rel has_lt.lt] (h : ∀ (x y : α), x y y x) :

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations

Function lattices #

@[instance]
def pi.has_sup {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_sup (α' i)] :
has_sup (Π (i : ι), α' i)
Equations
@[simp]
theorem pi.sup_apply {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_sup (α' i)] (f g : Π (i : ι), α' i) (i : ι) :
(f g) i = f i g i
theorem pi.sup_def {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_sup (α' i)] (f g : Π (i : ι), α' i) :
f g = λ (i : ι), f i g i
@[instance]
def pi.has_inf {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_inf (α' i)] :
has_inf (Π (i : ι), α' i)
Equations
@[simp]
theorem pi.inf_apply {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_inf (α' i)] (f g : Π (i : ι), α' i) (i : ι) :
(f g) i = f i g i
theorem pi.inf_def {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_inf (α' i)] (f g : Π (i : ι), α' i) :
f g = λ (i : ι), f i g i
@[instance]
def pi.semilattice_sup {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), semilattice_sup (α' i)] :
semilattice_sup (Π (i : ι), α' i)
Equations
@[instance]
def pi.semilattice_inf {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), semilattice_inf (α' i)] :
semilattice_inf (Π (i : ι), α' i)
Equations
@[instance]
def pi.lattice {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), lattice (α' i)] :
lattice (Π (i : ι), α' i)
Equations
@[instance]
def pi.distrib_lattice {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), distrib_lattice (α' i)] :
distrib_lattice (Π (i : ι), α' i)
Equations

Monotone functions and lattices #

theorem monotone.sup {α : Type u} {β : Type v} [preorder α] [semilattice_sup β] {f g : α → β} (hf : monotone f) (hg : monotone g) :

Pointwise supremum of two monotone functions is a monotone function.

theorem monotone.inf {α : Type u} {β : Type v} [preorder α] [semilattice_inf β] {f g : α → β} (hf : monotone f) (hg : monotone g) :

Pointwise infimum of two monotone functions is a monotone function.

theorem monotone.max {α : Type u} {β : Type v} [preorder α] [linear_order β] {f g : α → β} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : α), max (f x) (g x))

Pointwise maximum of two monotone functions is a monotone function.

theorem monotone.min {α : Type u} {β : Type v} [preorder α] [linear_order β] {f g : α → β} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : α), min (f x) (g x))

Pointwise minimum of two monotone functions is a monotone function.

theorem monotone.le_map_sup {α : Type u} {β : Type v} [semilattice_sup α] [semilattice_sup β] {f : α → β} (h : monotone f) (x y : α) :
f x f y f (x y)
theorem monotone.map_sup {α : Type u} {β : Type v} [semilattice_sup α] [is_total α has_le.le] [semilattice_sup β] {f : α → β} (hf : monotone f) (x y : α) :
f (x y) = f x f y
theorem monotone.map_inf_le {α : Type u} {β : Type v} [semilattice_inf α] [semilattice_inf β] {f : α → β} (h : monotone f) (x y : α) :
f (x y) f x f y
theorem monotone.map_inf {α : Type u} {β : Type v} [semilattice_inf α] [is_total α has_le.le] [semilattice_inf β] {f : α → β} (hf : monotone f) (x y : α) :
f (x y) = f x f y

Products of (semi-)lattices #

@[instance]
def prod.has_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] :
has_sup × β)
Equations
@[instance]
def prod.has_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] :
has_inf × β)
Equations
@[instance]
def prod.semilattice_sup (α : Type u) (β : Type v) [semilattice_sup α] [semilattice_sup β] :
Equations
@[instance]
def prod.semilattice_inf (α : Type u) (β : Type v) [semilattice_inf α] [semilattice_inf β] :
Equations
@[instance]
def prod.lattice (α : Type u) (β : Type v) [lattice α] [lattice β] :
lattice × β)
Equations
@[instance]
def prod.distrib_lattice (α : Type u) (β : Type v) [distrib_lattice α] [distrib_lattice β] :
Equations

Subtypes of (semi-)lattices #

def subtype.semilattice_sup {α : Type u} [semilattice_sup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) :
semilattice_sup {x // P x}

A subtype forms a -semilattice if preserves the property. See note [reducible non-instances].

Equations
def subtype.semilattice_inf {α : Type u} [semilattice_inf α] {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) :
semilattice_inf {x // P x}

A subtype forms a -semilattice if preserves the property. See note [reducible non-instances].

Equations
def subtype.lattice {α : Type u} [lattice α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) :
lattice {x // P x}

A subtype forms a lattice if and preserve the property. See note [reducible non-instances].

Equations