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

source
theorem le_antisymm' {α : Type u} [partial_order α] {a b : α} :
(:a ≤ b:) → b ≤ a → a = b
source
@[class]
structure has_sup (α : Type u) :
Type u
  • sup : α → α → α

Typeclass for the ⊔ (\lub) notation

Instances
source
@[class]
structure has_inf (α : Type u) :
Type u
  • inf : α → α → α

Typeclass for the ⊓ (\glb) notation

Instances

Join-semilattices #

source
@[class]
structure semilattice_sup (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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
source
@[instance]
def semilattice_sup.to_has_sup (α : Type u) [self : semilattice_sup α] :
has_sup α
source
@[instance]
def semilattice_sup.to_partial_order (α : Type u) [self : semilattice_sup α] :
partial_order α
source
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) :
semilattice_sup α

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
source
@[protected, instance]
def order_dual.has_sup (α : Type u_1) [has_inf α] :
has_sup (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_inf (α : Type u_1) [has_sup α] :
has_inf (order_dual α)
Equations
source
@[simp]
theorem le_sup_left {α : Type u} [semilattice_sup α] {a b : α} :
a ≤ a ⊔ b
source
theorem le_sup_left' {α : Type u} [semilattice_sup α] {a b : α} :
a ≤ (:a ⊔ b:)
source
@[simp]
theorem le_sup_right {α : Type u} [semilattice_sup α] {a b : α} :
b ≤ a ⊔ b
source
theorem le_sup_right' {α : Type u} [semilattice_sup α] {a b : α} :
b ≤ (:a ⊔ b:)
source
theorem le_sup_of_le_left {α : Type u} [semilattice_sup α] {a b c : α} (h : c ≤ a) :
c ≤ a ⊔ b
source
theorem le_sup_of_le_right {α : Type u} [semilattice_sup α] {a b c : α} (h : c ≤ b) :
c ≤ a ⊔ b
source
theorem sup_le {α : Type u} [semilattice_sup α] {a b c : α} :
a ≤ c → b ≤ c → a ⊔ b ≤ c
source
@[simp]
theorem sup_le_iff {α : Type u} [semilattice_sup α] {a b c : α} :
a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c
source
@[simp]
theorem sup_eq_left {α : Type u} [semilattice_sup α] {a b : α} :
a ⊔ b = a ↔ b ≤ a
source
theorem sup_of_le_left {α : Type u} [semilattice_sup α] {a b : α} (h : b ≤ a) :
a ⊔ b = a
source
@[simp]
theorem left_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
a = a ⊔ b ↔ b ≤ a
source
@[simp]
theorem sup_eq_right {α : Type u} [semilattice_sup α] {a b : α} :
a ⊔ b = b ↔ a ≤ b
source
theorem sup_of_le_right {α : Type u} [semilattice_sup α] {a b : α} (h : a ≤ b) :
a ⊔ b = b
source
@[simp]
theorem right_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
b = a ⊔ b ↔ a ≤ b
source
theorem sup_le_sup {α : Type u} [semilattice_sup α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a ⊔ c ≤ b ⊔ d
source
theorem sup_le_sup_left {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a ≤ b) (c : α) :
c ⊔ a ≤ c ⊔ b
source
theorem sup_le_sup_right {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a ≤ b) (c : α) :
a ⊔ c ≤ b ⊔ c
source
theorem le_of_sup_eq {α : Type u} [semilattice_sup α] {a b : α} (h : a ⊔ b = b) :
a ≤ b
source
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)
source
@[simp]
theorem sup_lt_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
b ⊔ c < a ↔ b < a ∧ c < a
source
@[simp]
theorem le_sup_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
source
@[simp]
theorem lt_sup_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :
a < b ⊔ c ↔ a < b ∨ a < c
source
@[simp]
theorem sup_idem {α : Type u} [semilattice_sup α] {a : α} :
a ⊔ a = a
source
@[protected, instance]
def sup_is_idempotent {α : Type u} [semilattice_sup α] :
is_idempotent α has_sup.sup
source
theorem sup_comm {α : Type u} [semilattice_sup α] {a b : α} :
a ⊔ b = b ⊔ a
source
@[protected, instance]
def sup_is_commutative {α : Type u} [semilattice_sup α] :
is_commutative α has_sup.sup
source
theorem sup_assoc {α : Type u} [semilattice_sup α] {a b c : α} :
a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
source
@[protected, instance]
def sup_is_associative {α : Type u} [semilattice_sup α] :
is_associative α has_sup.sup
source
theorem sup_left_right_swap {α : Type u} [semilattice_sup α] (a b c : α) :
a ⊔ b ⊔ c = c ⊔ b ⊔ a
source
@[simp]
theorem sup_left_idem {α : Type u} [semilattice_sup α] {a b : α} :
a ⊔ (a ⊔ b) = a ⊔ b
source
@[simp]
theorem sup_right_idem {α : Type u} [semilattice_sup α] {a b : α} :
a ⊔ b ⊔ b = a ⊔ b
source
theorem sup_left_comm {α : Type u} [semilattice_sup α] (a b c : α) :
a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)
source
theorem sup_right_comm {α : Type u} [semilattice_sup α] (a b c : α) :
a ⊔ b ⊔ c = a ⊔ c ⊔ b
source
theorem sup_sup_sup_comm {α : Type u} [semilattice_sup α] (a b c d : α) :
a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
source
theorem forall_le_or_exists_lt_sup {α : Type u} [semilattice_sup α] (a : α) :
(∀ (b : α), b ≤ a) ∨ ∃ (b : α), a < b
source
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.

source
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
source
theorem semilattice_sup.ext {α : Type u_1} {A B : semilattice_sup α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A = B
source
theorem exists_lt_of_sup (α : Type u_1) [semilattice_sup α] [nontrivial α] :
∃ (a b : α), a < b
source
theorem ite_le_sup {α : Type u} [semilattice_sup α] (s s' : α) (P : Prop) [decidable P] :
ite P s s' ≤ s ⊔ s'

Meet-semilattices #

source
@[instance]
def semilattice_inf.to_has_inf (α : Type u) [self : semilattice_inf α] :
has_inf α
source
@[class]
structure semilattice_inf (α : Type u) :
Type u
  • inf : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
  • inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
  • le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ 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
source
@[instance]
def semilattice_inf.to_partial_order (α : Type u) [self : semilattice_inf α] :
partial_order α
source
@[protected, instance]
def order_dual.semilattice_sup (α : Type u_1) [semilattice_inf α] :
semilattice_sup (order_dual α)
Equations
source
@[protected, instance]
def order_dual.semilattice_inf (α : Type u_1) [semilattice_sup α] :
semilattice_inf (order_dual α)
Equations
source
theorem semilattice_sup.dual_dual (α : Type u_1) [H : semilattice_sup α] :
order_dual.semilattice_sup (order_dual α) = H
source
@[simp]
theorem inf_le_left {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b ≤ a
source
theorem inf_le_left' {α : Type u} [semilattice_inf α] {a b : α} :
(:a ⊓ b:) ≤ a
source
@[simp]
theorem inf_le_right {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b ≤ b
source
theorem inf_le_right' {α : Type u} [semilattice_inf α] {a b : α} :
(:a ⊓ b:) ≤ b
source
theorem le_inf {α : Type u} [semilattice_inf α] {a b c : α} :
a ≤ b → a ≤ c → a ≤ b ⊓ c
source
theorem inf_le_of_left_le {α : Type u} [semilattice_inf α] {a b c : α} (h : a ≤ c) :
a ⊓ b ≤ c
source
theorem inf_le_of_right_le {α : Type u} [semilattice_inf α] {a b c : α} (h : b ≤ c) :
a ⊓ b ≤ c
source
@[simp]
theorem le_inf_iff {α : Type u} [semilattice_inf α] {a b c : α} :
a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c
source
@[simp]
theorem inf_eq_left {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b = a ↔ a ≤ b
source
theorem inf_of_le_left {α : Type u} [semilattice_inf α] {a b : α} (h : a ≤ b) :
a ⊓ b = a
source
@[simp]
theorem left_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
a = a ⊓ b ↔ a ≤ b
source
@[simp]
theorem inf_eq_right {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b = b ↔ b ≤ a
source
theorem inf_of_le_right {α : Type u} [semilattice_inf α] {a b : α} (h : b ≤ a) :
a ⊓ b = b
source
@[simp]
theorem right_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
b = a ⊓ b ↔ b ≤ a
source
theorem inf_le_inf {α : Type u} [semilattice_inf α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a ⊓ c ≤ b ⊓ d
source
theorem inf_le_inf_right {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b ≤ c) :
b ⊓ a ≤ c ⊓ a
source
theorem inf_le_inf_left {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b ≤ c) :
a ⊓ b ≤ a ⊓ c
source
theorem le_of_inf_eq {α : Type u} [semilattice_inf α] {a b : α} (h : a ⊓ b = a) :
a ≤ b
source
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)
source
@[simp]
theorem lt_inf_iff {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b c : α} :
a < b ⊓ c ↔ a < b ∧ a < c
source
@[simp]
theorem inf_le_iff {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b c : α} :
b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a
source
@[simp]
theorem inf_idem {α : Type u} [semilattice_inf α] {a : α} :
a ⊓ a = a
source
@[protected, instance]
def inf_is_idempotent {α : Type u} [semilattice_inf α] :
is_idempotent α has_inf.inf
source
theorem inf_comm {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b = b ⊓ a
source
@[protected, instance]
def inf_is_commutative {α : Type u} [semilattice_inf α] :
is_commutative α has_inf.inf
source
theorem inf_assoc {α : Type u} [semilattice_inf α] {a b c : α} :
a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
source
@[protected, instance]
def inf_is_associative {α : Type u} [semilattice_inf α] :
is_associative α has_inf.inf
source
theorem inf_left_right_swap {α : Type u} [semilattice_inf α] (a b c : α) :
a ⊓ b ⊓ c = c ⊓ b ⊓ a
source
@[simp]
theorem inf_left_idem {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ (a ⊓ b) = a ⊓ b
source
@[simp]
theorem inf_right_idem {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b ⊓ b = a ⊓ b
source
theorem inf_left_comm {α : Type u} [semilattice_inf α] (a b c : α) :
a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)
source
theorem inf_right_comm {α : Type u} [semilattice_inf α] (a b c : α) :
a ⊓ b ⊓ c = a ⊓ c ⊓ b
source
theorem inf_inf_inf_comm {α : Type u} [semilattice_inf α] (a b c d : α) :
a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)
source
theorem forall_le_or_exists_lt_inf {α : Type u} [semilattice_inf α] (a : α) :
(∀ (b : α), a ≤ b) ∨ ∃ (b : α), b < a
source
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
source
theorem semilattice_inf.ext {α : Type u_1} {A B : semilattice_inf α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A = B
source
theorem semilattice_inf.dual_dual (α : Type u_1) [H : semilattice_inf α] :
order_dual.semilattice_inf (order_dual α) = H
source
theorem exists_lt_of_inf (α : Type u_1) [semilattice_inf α] [nontrivial α] :
∃ (a b : α), a < b
source
theorem inf_le_ite {α : Type u} [semilattice_inf α] (s s' : α) (P : Prop) [decidable P] :
s ⊓ s' ≤ ite P s s'
source
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) :
semilattice_inf α

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 #

source
@[instance]
def lattice.to_semilattice_inf (α : Type u) [self : lattice α] :
semilattice_inf α
source
@[instance]
def lattice.to_semilattice_sup (α : Type u) [self : lattice α] :
semilattice_sup α
source
@[class]
structure lattice (α : Type u) :
Type u
  • sup : α → α → α
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ b ⊓ c

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

Instances
source
@[protected, instance]
def order_dual.lattice (α : Type u_1) [lattice α] :
lattice (order_dual α)
Equations
source
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) :
semilattice_sup.to_partial_order α = semilattice_inf.to_partial_order α

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

source
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) :
lattice α

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
source
theorem inf_le_sup {α : Type u} [lattice α] {a b : α} :
a ⊓ b ≤ a ⊔ b
source
@[simp]
theorem inf_lt_sup {α : Type u} [lattice α] {a b : α} :
a ⊓ b < a ⊔ b ↔ a ≠ b

Distributivity laws #

source
theorem sup_inf_le {α : Type u} [lattice α] {a b c : α} :
a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c)
source
theorem le_inf_sup {α : Type u} [lattice α] {a b c : α} :
a ⊓ b ⊔ a ⊓ c ≤ a ⊓ (b ⊔ c)
source
theorem inf_sup_self {α : Type u} [lattice α] {a b : α} :
a ⊓ (a ⊔ b) = a
source
theorem sup_inf_self {α : Type u} [lattice α] {a b : α} :
a ⊔ a ⊓ b = a
source
theorem sup_eq_iff_inf_eq {α : Type u} [lattice α] {a b : α} :
a ⊔ b = b ↔ a ⊓ b = a
source
theorem lattice.ext {α : Type u_1} {A B : lattice α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :
A = B

Distributive lattices #

source
@[instance]
def distrib_lattice.to_lattice (α : Type u_1) [self : distrib_lattice α] :
lattice α
source
@[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 ≤ b → b ≤ c → a ≤ c
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
  • le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
  • sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ 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 ≤ b → a ≤ c → a ≤ 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
source
theorem le_sup_inf {α : Type u} [distrib_lattice α] {x y z : α} :
(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
source
theorem sup_inf_left {α : Type u} [distrib_lattice α] {x y z : α} :
x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)
source
theorem sup_inf_right {α : Type u} [distrib_lattice α] {x y z : α} :
y ⊓ z ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)
source
theorem inf_sup_left {α : Type u} [distrib_lattice α] {x y z : α} :
x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z
source
@[protected, instance]
def order_dual.distrib_lattice (α : Type u_1) [distrib_lattice α] :
distrib_lattice (order_dual α)
Equations
source
theorem inf_sup_right {α : Type u} [distrib_lattice α] {x y z : α} :
(y ⊔ z) ⊓ x = y ⊓ x ⊔ z ⊓ x
source
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
source
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 #

source
@[protected, instance]
def lattice_of_linear_order {α : Type u} [o : linear_order α] :
lattice α
Equations
source
theorem sup_eq_max {α : Type u} [linear_order α] {x y : α} :
x ⊔ y = max x y
source
theorem inf_eq_min {α : Type u} [linear_order α] {x y : α} :
x ⊓ y = min x y
source
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) :
linear_order α

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations
source
@[protected, instance]
def distrib_lattice_of_linear_order {α : Type u} [o : linear_order α] :
distrib_lattice α
Equations
source
@[protected, instance]
def nat.distrib_lattice  :
distrib_lattice ℕ
Equations

Function lattices #

source
@[protected, instance]
def pi.has_sup {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_sup (α' i)] :
has_sup (Π (i : ι), α' i)
Equations
source
@[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
source
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
source
@[protected, instance]
def pi.has_inf {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_inf (α' i)] :
has_inf (Π (i : ι), α' i)
Equations
source
@[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
source
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
source
@[protected, instance]
def pi.semilattice_sup {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), semilattice_sup (α' i)] :
semilattice_sup (Π (i : ι), α' i)
Equations
source
@[protected, instance]
def pi.semilattice_inf {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), semilattice_inf (α' i)] :
semilattice_inf (Π (i : ι), α' i)
Equations
source
@[protected, instance]
def pi.lattice {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), lattice (α' i)] :
lattice (Π (i : ι), α' i)
Equations
source
@[protected, instance]
def pi.distrib_lattice {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), distrib_lattice (α' i)] :
distrib_lattice (Π (i : ι), α' i)
Equations

Monotone functions and lattices #

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

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

source
@[protected]
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.

source
@[protected]
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.

source
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)
source
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
source
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
source
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 #

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

Subtypes of (semi-)lattices #

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

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

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

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

Equations
source
@[protected]
def subtype.lattice {α : Type u} [lattice α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) :
lattice {x // P x}

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

Equations
source
@[protected]
def function.injective.semilattice_sup {α : Type u} {β : Type v} [has_sup α] [semilattice_sup β] (f : α → β) (hf_inj : function.injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) :
semilattice_sup α

A type endowed with ⊔ is a semilattice_sup, if it admits an injective map that preserves ⊔ to a semilattice_sup. See note [reducible non-instances].

Equations
source
@[protected]
def function.injective.semilattice_inf {α : Type u} {β : Type v} [has_inf α] [semilattice_inf β] (f : α → β) (hf_inj : function.injective f) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) :
semilattice_inf α

A type endowed with ⊓ is a semilattice_inf, if it admits an injective map that preserves ⊓ to a semilattice_inf. See note [reducible non-instances].

Equations
source
@[protected]
def function.injective.lattice {α : Type u} {β : Type v} [has_sup α] [has_inf α] [lattice β] (f : α → β) (hf_inj : function.injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) :
lattice α

A type endowed with ⊔ and ⊓ is a lattice, if it admits an injective map that preserves ⊔ and ⊓ to a lattice. See note [reducible non-instances].

Equations
source
@[protected]
def function.injective.distrib_lattice {α : Type u} {β : Type v} [has_sup α] [has_inf α] [distrib_lattice β] (f : α → β) (hf_inj : function.injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) :
distrib_lattice α

A type endowed with ⊔ and ⊓ is a distrib_lattice, if it admits an injective map that preserves ⊔ and ⊓ to a distrib_lattice. See note [reducible non-instances].

Equations