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 #

• semilattice_sup: a type class for join semilattices

• semilattice_sup.mk': an alternative constructor for semilattice_sup via proofs that ⊔ is commutative, associative and idempotent.

• semilattice_inf: a type class for meet semilattices

• semilattice_sup.mk': an alternative constructor for semilattice_inf via proofs that ⊓ is commutative, associative and idempotent.

• lattice: a type class for lattices

• lattice.mk': an alternative constructor for lattice via profs that ⊔ and ⊓ are commutative, associative and satisfy a pair of "absorption laws".

• distrib_lattice: a type class for distributive lattices.

## Notations #

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

## TODO #

• (Semi-)lattice homomorphisms
• Alternative constructors for distributive lattices from the other distributive properties

## Tags #

semilattice, lattice

theorem le_antisymm' {α : Type u} {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 of this typeclass
Instances of other typeclasses for semilattice_sup
• semilattice_sup.has_sizeof_inst
@[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
@[protected, instance]
def order_dual.has_sup (α : Type u_1) [has_inf α] :
Equations
@[protected, instance]
def order_dual.has_inf (α : Type u_1) [has_sup α] :
Equations
@[simp]
theorem le_sup_left {α : Type u} {a b : α} :
a a b
theorem le_sup_left' {α : Type u} {a b : α} :
a (:a b:)
@[simp]
theorem le_sup_right {α : Type u} {a b : α} :
b a b
theorem le_sup_right' {α : Type u} {a b : α} :
b (:a b:)
theorem le_sup_of_le_left {α : Type u} {a b c : α} (h : c a) :
c a b
theorem le_sup_of_le_right {α : Type u} {a b c : α} (h : c b) :
c a b
theorem lt_sup_of_lt_left {α : Type u} {a b c : α} (h : c < a) :
c < a b
theorem lt_sup_of_lt_right {α : Type u} {a b c : α} (h : c < b) :
c < a b
theorem sup_le {α : Type u} {a b c : α} :
a cb ca b c
@[simp]
theorem sup_le_iff {α : Type u} {a b c : α} :
a b c a c b c
@[simp]
theorem sup_eq_left {α : Type u} {a b : α} :
a b = a b a
theorem sup_of_le_left {α : Type u} {a b : α} (h : b a) :
a b = a
@[simp]
theorem left_eq_sup {α : Type u} {a b : α} :
a = a b b a
@[simp]
theorem left_lt_sup {α : Type u} {a b : α} :
a < a b ¬b a
@[simp]
theorem sup_eq_right {α : Type u} {a b : α} :
a b = b a b
theorem sup_of_le_right {α : Type u} {a b : α} (h : a b) :
a b = b
@[simp]
theorem right_eq_sup {α : Type u} {a b : α} :
b = a b a b
@[simp]
theorem right_lt_sup {α : Type u} {a b : α} :
b < a b ¬a b
theorem left_or_right_lt_sup {α : Type u} {a b : α} (h : a b) :
a < a b b < a b
theorem le_iff_exists_sup {α : Type u} {a b : α} :
a b ∃ (c : α), b = a c
theorem sup_le_sup {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c d) :
a c b d
theorem sup_le_sup_left {α : Type u} {a b : α} (h₁ : a b) (c : α) :
c a c b
theorem sup_le_sup_right {α : Type u} {a b : α} (h₁ : a b) (c : α) :
a c b c
theorem le_of_sup_eq {α : Type u} {a b : α} (h : a b = b) :
a b
@[simp]
theorem sup_idem {α : Type u} {a : α} :
a a = a
@[protected, instance]
def sup_is_idempotent {α : Type u}  :
theorem sup_comm {α : Type u} {a b : α} :
a b = b a
@[protected, instance]
def sup_is_commutative {α : Type u}  :
theorem sup_assoc {α : Type u} {a b c : α} :
a b c = a (b c)
@[protected, instance]
def sup_is_associative {α : Type u}  :
theorem sup_left_right_swap {α : Type u} (a b c : α) :
a b c = c b a
@[simp]
theorem sup_left_idem {α : Type u} {a b : α} :
a (a b) = a b
@[simp]
theorem sup_right_idem {α : Type u} {a b : α} :
a b b = a b
theorem sup_left_comm {α : Type u} (a b c : α) :
a (b c) = b (a c)
theorem sup_right_comm {α : Type u} (a b c : α) :
a b c = a c b
theorem sup_sup_sup_comm {α : Type u} (a b c d : α) :
a b (c d) = a c (b d)
theorem sup_sup_distrib_left {α : Type u} (a b c : α) :
a (b c) = a b (a c)
theorem sup_sup_distrib_right {α : Type u} (a b c : α) :
a b c = a c (b c)
theorem sup_congr_left {α : Type u} {a b c : α} (hb : b a c) (hc : c a b) :
a b = a c
theorem sup_congr_right {α : Type u} {a b c : α} (ha : a b c) (hb : b a c) :
a c = b c
theorem sup_eq_sup_iff_left {α : Type u} {a b c : α} :
a b = a c b a c c a b
theorem sup_eq_sup_iff_right {α : Type u} {a b c : α} :
a c = b c a b c b a c
theorem monotone.forall_le_of_antitone {α : Type u} {β : 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
theorem ite_le_sup {α : Type u} (s s' : α) (P : Prop) [decidable P] :
ite P s s' s s'

### 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 of this typeclass
Instances of other typeclasses for semilattice_inf
• semilattice_inf.has_sizeof_inst
@[instance]
def semilattice_inf.to_partial_order (α : Type u) [self : semilattice_inf α] :
@[protected, instance]
def order_dual.semilattice_sup (α : Type u_1)  :
Equations
@[protected, instance]
def order_dual.semilattice_inf (α : Type u_1)  :
Equations
theorem semilattice_sup.dual_dual (α : Type u_1) [H : semilattice_sup α] :
@[simp]
theorem inf_le_left {α : Type u} {a b : α} :
a b a
theorem inf_le_left' {α : Type u} {a b : α} :
(:a b:) a
@[simp]
theorem inf_le_right {α : Type u} {a b : α} :
a b b
theorem inf_le_right' {α : Type u} {a b : α} :
(:a b:) b
theorem le_inf {α : Type u} {a b c : α} :
a ba ca b c
theorem inf_le_of_left_le {α : Type u} {a b c : α} (h : a c) :
a b c
theorem inf_le_of_right_le {α : Type u} {a b c : α} (h : b c) :
a b c
theorem inf_lt_of_left_lt {α : Type u} {a b c : α} (h : a < c) :
a b < c
theorem inf_lt_of_right_lt {α : Type u} {a b c : α} (h : b < c) :
a b < c
@[simp]
theorem le_inf_iff {α : Type u} {a b c : α} :
a b c a b a c
@[simp]
theorem inf_eq_left {α : Type u} {a b : α} :
a b = a a b
@[simp]
theorem inf_lt_left {α : Type u} {a b : α} :
a b < a ¬a b
theorem inf_of_le_left {α : Type u} {a b : α} (h : a b) :
a b = a
@[simp]
theorem left_eq_inf {α : Type u} {a b : α} :
a = a b a b
@[simp]
theorem inf_eq_right {α : Type u} {a b : α} :
a b = b b a
@[simp]
theorem inf_lt_right {α : Type u} {a b : α} :
a b < b ¬b a
theorem inf_lt_left_or_right {α : Type u} {a b : α} (h : a b) :
a b < a a b < b
theorem inf_of_le_right {α : Type u} {a b : α} (h : b a) :
a b = b
@[simp]
theorem right_eq_inf {α : Type u} {a b : α} :
b = a b b a
theorem inf_le_inf {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c d) :
a c b d
theorem inf_le_inf_right {α : Type u} (a : α) {b c : α} (h : b c) :
b a c a
theorem inf_le_inf_left {α : Type u} (a : α) {b c : α} (h : b c) :
a b a c
theorem le_of_inf_eq {α : Type u} {a b : α} (h : a b = a) :
a b
@[simp]
theorem inf_idem {α : Type u} {a : α} :
a a = a
@[protected, instance]
def inf_is_idempotent {α : Type u}  :
theorem inf_comm {α : Type u} {a b : α} :
a b = b a
@[protected, instance]
def inf_is_commutative {α : Type u}  :
theorem inf_assoc {α : Type u} {a b c : α} :
a b c = a (b c)
@[protected, instance]
def inf_is_associative {α : Type u}  :
theorem inf_left_right_swap {α : Type u} (a b c : α) :
a b c = c b a
@[simp]
theorem inf_left_idem {α : Type u} {a b : α} :
a (a b) = a b
@[simp]
theorem inf_right_idem {α : Type u} {a b : α} :
a b b = a b
theorem inf_left_comm {α : Type u} (a b c : α) :
a (b c) = b (a c)
theorem inf_right_comm {α : Type u} (a b c : α) :
a b c = a c b
theorem inf_inf_inf_comm {α : Type u} (a b c d : α) :
a b (c d) = a c (b d)
theorem inf_inf_distrib_left {α : Type u} (a b c : α) :
a (b c) = a b (a c)
theorem inf_inf_distrib_right {α : Type u} (a b c : α) :
a b c = a c (b c)
theorem inf_congr_left {α : Type u} {a b c : α} (hb : a c b) (hc : a b c) :
a b = a c
theorem inf_congr_right {α : Type u} {a b c : α} (h1 : b c a) (h2 : a c b) :
a c = b c
theorem inf_eq_inf_iff_left {α : Type u} {a b c : α} :
a b = a c a c b a b c
theorem inf_eq_inf_iff_right {α : Type u} {a b c : α} :
a c = b c b c a a c b
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
theorem semilattice_inf.dual_dual (α : Type u_1) [H : semilattice_inf α] :
theorem inf_le_ite {α : Type u} (s s' : α) (P : Prop) [decidable P] :
s s' ite P s s'
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 of this typeclass
Instances of other typeclasses for lattice
• lattice.has_sizeof_inst
@[protected, instance]
def order_dual.lattice (α : Type u_1) [lattice α] :
Equations
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
theorem inf_le_sup {α : Type u} [lattice α] {a b : α} :
a b a b
@[simp]
theorem inf_lt_sup {α : Type u} [lattice α] {a b : α} :
a b < a b a 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 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 α] :
Instances for distrib_lattice.to_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). To prove distributivity from the dual law, use distrib_lattice.of_inf_sup_le.

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 of this typeclass
Instances of other typeclasses for distrib_lattice
• distrib_lattice.has_sizeof_inst
theorem le_sup_inf {α : Type u} {x y z : α} :
(x y) (x z) x y z
theorem sup_inf_left {α : Type u} {x y z : α} :
x y z = (x y) (x z)
theorem sup_inf_right {α : Type u} {x y z : α} :
y z x = (y x) (z x)
theorem inf_sup_left {α : Type u} {x y z : α} :
x (y z) = x y x z
@[protected, instance]
def order_dual.distrib_lattice (α : Type u_1)  :
Equations
theorem inf_sup_right {α : Type u} {x y z : α} :
(y z) x = y x z x
theorem le_of_inf_le_sup_le {α : Type u} {x y z : α} (h₁ : x z y z) (h₂ : x z y z) :
x y
theorem eq_of_inf_eq_sup_eq {α : Type u} {a b c : α} (h₁ : b a = c a) (h₂ : b a = c a) :
b = c
@[reducible]
def distrib_lattice.of_inf_sup_le {α : Type u} [lattice α] (inf_sup_le : ∀ (a b c : α), a (b c) a b a c) :

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

Equations

### Lattices derived from linear orders #

@[protected, instance]
def linear_order.to_lattice {α : Type u} [o : linear_order α] :
Equations
theorem sup_eq_max {α : Type u} [linear_order α] {a b : α} :
a b =
theorem inf_eq_min {α : Type u} [linear_order α] {a b : α} :
a b =
theorem sup_ind {α : Type u} [linear_order α] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) :
p (a b)
@[simp]
theorem le_sup_iff {α : Type u} [linear_order α] {a b c : α} :
a b c a b a c
@[simp]
theorem lt_sup_iff {α : Type u} [linear_order α] {a b c : α} :
a < b c a < b a < c
@[simp]
theorem sup_lt_iff {α : Type u} [linear_order α] {a b c : α} :
b c < a b < a c < a
theorem inf_ind {α : Type u} [linear_order α] (a b : α) {p : α → Prop} :
p ap bp (a b)
@[simp]
theorem inf_le_iff {α : Type u} [linear_order α] {a b c : α} :
b c a b a c a
@[simp]
theorem inf_lt_iff {α : Type u} [linear_order α] {a b c : α} :
b c < a b < a c < a
@[simp]
theorem lt_inf_iff {α : Type u} [linear_order α] {a b c : α} :
a < b c a < b a < c
theorem sup_eq_max_default {α : Type u}  :
theorem inf_eq_min_default {α : Type u}  :
@[reducible]
def lattice.to_linear_order (α : Type u) [lattice α] [decidable_eq α]  :

A lattice with total order is a linear order.

Equations
@[protected, instance]
def linear_order.to_distrib_lattice {α : Type u} [o : linear_order α] :
Equations
@[protected, instance]
Equations

### Dual order #

@[simp]
theorem of_dual_inf {α : Type u} [has_sup α] (a b : αᵒᵈ) :
@[simp]
theorem of_dual_sup {α : Type u} [has_inf α] (a b : αᵒᵈ) :
@[simp]
theorem to_dual_inf {α : Type u} [has_inf α] (a b : α) :
@[simp]
theorem to_dual_sup {α : Type u} [has_sup α] (a b : α) :
@[simp]
theorem of_dual_min {α : Type u} [linear_order α] (a b : αᵒᵈ) :
@[simp]
theorem of_dual_max {α : Type u} [linear_order α] (a b : αᵒᵈ) :
@[simp]
theorem to_dual_min {α : Type u} [linear_order α] (a b : α) :
@[simp]
theorem to_dual_max {α : Type u} [linear_order α] (a b : α) :

### Function lattices #

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

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

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

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

Pointwise maximum of two monotone functions is a monotone function.

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

Pointwise minimum of two monotone functions is a monotone function.

theorem monotone.le_map_sup {α : Type u} {β : Type v} {f : α → β} (h : monotone f) (x y : α) :
f x f y f (x y)
theorem monotone.map_inf_le {α : Type u} {β : Type v} {f : α → β} (h : monotone f) (x y : α) :
f (x y) f x f y
theorem monotone.of_map_inf {α : Type u} {β : Type v} {f : α → β} (h : ∀ (x y : α), f (x y) = f x f y) :
theorem monotone.of_map_sup {α : Type u} {β : Type v} {f : α → β} (h : ∀ (x y : α), f (x y) = f x f y) :
theorem monotone.map_sup {α : Type u} {β : Type v} [linear_order α] {f : α → β} (hf : monotone f) (x y : α) :
f (x y) = f x f y
theorem monotone.map_inf {α : Type u} {β : Type v} [linear_order α] {f : α → β} (hf : monotone f) (x y : α) :
f (x y) = f x f y
@[protected]
theorem monotone_on.sup {α : Type u} {β : Type v} [preorder α] {f g : α → β} {s : set α} (hf : s) (hg : s) :

Pointwise supremum of two monotone functions is a monotone function.

@[protected]
theorem monotone_on.inf {α : Type u} {β : Type v} [preorder α] {f g : α → β} {s : set α} (hf : s) (hg : s) :

Pointwise infimum of two monotone functions is a monotone function.

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

Pointwise maximum of two monotone functions is a monotone function.

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

Pointwise minimum of two monotone functions is a monotone function.

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

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

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

Pointwise maximum of two monotone functions is a monotone function.

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

Pointwise minimum of two monotone functions is a monotone function.

theorem antitone.map_sup_le {α : Type u} {β : Type v} {f : α → β} (h : antitone f) (x y : α) :
f (x y) f x f y
theorem antitone.le_map_inf {α : Type u} {β : Type v} {f : α → β} (h : antitone f) (x y : α) :
f x f y f (x y)
theorem antitone.map_sup {α : Type u} {β : Type v} [linear_order α] {f : α → β} (hf : antitone f) (x y : α) :
f (x y) = f x f y
theorem antitone.map_inf {α : Type u} {β : Type v} [linear_order α] {f : α → β} (hf : antitone f) (x y : α) :
f (x y) = f x f y
@[protected]
theorem antitone_on.sup {α : Type u} {β : Type v} [preorder α] {f g : α → β} {s : set α} (hf : s) (hg : s) :

Pointwise supremum of two antitone functions is a antitone function.

@[protected]
theorem antitone_on.inf {α : Type u} {β : Type v} [preorder α] {f g : α → β} {s : set α} (hf : s) (hg : s) :

Pointwise infimum of two antitone functions is a antitone function.

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

Pointwise maximum of two antitone functions is a antitone function.

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

Pointwise minimum of two antitone functions is a antitone function.

### Products of (semi-)lattices #

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

### Subtypes of (semi-)lattices #

@[protected, reducible]
def subtype.semilattice_sup {α : Type u} {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
@[protected, reducible]
def subtype.semilattice_inf {α : Type u} {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
@[protected, reducible]
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
@[simp, norm_cast]
theorem subtype.coe_sup {α : Type u} {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) (x y : subtype P) :
(x y) = x y
@[simp, norm_cast]
theorem subtype.coe_inf {α : Type u} {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) (x y : subtype P) :
(x y) = x y
@[simp]
theorem subtype.mk_sup_mk {α : Type u} {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) {x y : α} (hx : P x) (hy : P y) :
x, hx⟩ y, hy⟩ = x y, _⟩
@[simp]
theorem subtype.mk_inf_mk {α : Type u} {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) {x y : α} (hx : P x) (hy : P y) :
x, hx⟩ y, hy⟩ = x y, _⟩
@[protected, reducible]
def function.injective.semilattice_sup {α : Type u} {β : Type v} [has_sup α] (f : α → β) (hf_inj : function.injective f) (map_sup : ∀ (a b : α), f (a b) = f a f b) :

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
@[protected, reducible]
def function.injective.semilattice_inf {α : Type u} {β : Type v} [has_inf α] (f : α → β) (hf_inj : function.injective f) (map_inf : ∀ (a b : α), f (a b) = f a f b) :

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
@[protected, reducible]
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) :

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
@[protected, reducible]
def function.injective.distrib_lattice {α : Type u} {β : Type v} [has_sup α] [has_inf α] (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) :

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
@[protected, instance]
Equations