mathlib documentation

order.lattice

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

@[class]
structure semilattice_sup  :
Type uType u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), a c_1b c_1a b c_1

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) [s : semilattice_sup α] :

@[instance]

@[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_left_of_le {α : Type u} [semilattice_sup α] {a b c : α} :
c ac a b

theorem le_sup_right_of_le {α : Type u} [semilattice_sup α] {a b c : α} :
c bc 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 : α} :
b aa 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 : α} :
a ba 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 : α} :
a bc da 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 : α} :
a b = ba b

theorem sup_ind {α : Type u} [semilattice_sup α] [is_total α has_le.le] (a b : α) {p : α → Prop} :
p ap bp (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]

@[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 forall_le_or_exists_lt_sup {α : Type u} [semilattice_sup α] (a : α) :
(∀ (b : α), b a) ∃ (b : α), a < 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 α} :
(∀ (x y : α), x y x y)A = B

@[instance]
def semilattice_inf.to_has_inf (α : Type u) [s : semilattice_inf α] :

@[class]
structure semilattice_inf  :
Type uType u
  • inf : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), a ba c_1a b c_1

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]

@[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_left_of_le {α : Type u} [semilattice_inf α] {a b c : α} :
a ca b c

theorem inf_le_right_of_le {α : Type u} [semilattice_inf α] {a b c : α} :
b ca 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 : α} :
a ba 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 : α} :
b aa 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 : α} :
a bc da c b d

theorem inf_le_inf_right {α : Type u} [semilattice_inf α] (a : α) {b c : α} :
b cb a c a

theorem inf_le_inf_left {α : Type u} [semilattice_inf α] (a : α) {b c : α} :
b ca b a c

theorem le_of_inf_eq {α : Type u} [semilattice_inf α] {a b : α} :
a b = aa b

theorem inf_ind {α : Type u} [semilattice_inf α] [is_total α has_le.le] (a b : α) {p : α → Prop} :
p ap bp (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]

@[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 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 α} :
(∀ (x y : α), x y x y)A = B

Lattices

@[instance]
def lattice.to_semilattice_inf (α : Type u) [s : lattice α] :

@[instance]
def lattice.to_semilattice_sup (α : Type u) [s : lattice α] :

@[class]
structure lattice  :
Type uType u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), a c_1b c_1a b c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1

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

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

@[instance]
def distrib_lattice.to_lattice (α : Type u_1) [s : distrib_lattice α] :

@[class]
structure distrib_lattice  :
Type u_1Type u_1
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • 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_1 : α), a c_1b c_1a b c_1
  • inf : α → α → α
  • inf_le_left : ∀ (a b : α), a b a
  • inf_le_right : ∀ (a b : α), a b b
  • le_inf : ∀ (a b c_1 : α), a ba c_1a b c_1
  • 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 distribution properties (of sup over inf or inf over sup, on the left or right). 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 : α} :
x z y zx z y zx y

theorem eq_of_inf_eq_sup_eq {α : Type u} [distrib_lattice α] {a b c : α} :
b a = c ab a = c ab = c

Lattices derived from linear orders

theorem sup_eq_max {α : Type u} [decidable_linear_order α] {x y : α} :
x y = max x y

theorem inf_eq_min {α : Type u} [decidable_linear_order α] {x y : α} :
x y = min x y

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

@[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