# (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

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

• SemilatticeInf: a type class for meet semilattices

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

• Lattice: a type class for lattices

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

• DistribLattice: 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

See if the term is a ⊂ b and the goal is a ⊆ b.

Equations
Instances For

### Join-semilattices #

class SemilatticeSup (α : Type u) extends , :

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.

• 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
• le_antisymm : ∀ (a b : α), a bb aa = b
• le_sup_left : ∀ (a b : α), a a b

The supremum is an upper bound on the first argument

• le_sup_right : ∀ (a b : α), b a b

The supremum is an upper bound on the second argument

• sup_le : ∀ (a b c : α), a cb ca b c

The supremum is the least upper bound

Instances
theorem SemilatticeSup.le_sup_left {α : Type u} [self : ] (a : α) (b : α) :
a a b

The supremum is an upper bound on the first argument

theorem SemilatticeSup.le_sup_right {α : Type u} [self : ] (a : α) (b : α) :
b a b

The supremum is an upper bound on the second argument

theorem SemilatticeSup.sup_le {α : Type u} [self : ] (a : α) (b : α) (c : α) :
a cb ca b c

The supremum is the least upper bound

def SemilatticeSup.mk' {α : Type u_1} [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
Instances For
instance OrderDual.instSup (α : Type u_1) [Inf α] :
Equations
• = { sup := fun (x x_1 : α) => x x_1 }
instance OrderDual.instInf (α : Type u_1) [Sup α] :
Equations
• = { inf := fun (x x_1 : α) => x x_1 }
@[simp]
theorem le_sup_left {α : Type u} [] {a : α} {b : α} :
a a b
@[deprecated le_sup_left]
theorem le_sup_left' {α : Type u} [] {a : α} {b : α} :
a a b

Alias of le_sup_left.

@[simp]
theorem le_sup_right {α : Type u} [] {a : α} {b : α} :
b a b
@[deprecated le_sup_right]
theorem le_sup_right' {α : Type u} [] {a : α} {b : α} :
b a b

Alias of le_sup_right.

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
@[simp]
theorem sup_eq_right {α : Type u} [] {a : α} {b : α} :
a b = b a b
@[simp]
theorem left_eq_sup {α : Type u} [] {a : α} {b : α} :
a = a b b a
@[simp]
theorem right_eq_sup {α : Type u} [] {a : α} {b : α} :
b = a b a b
@[simp]
theorem sup_of_le_left {α : Type u} [] {a : α} {b : α} :
b aa b = a

Alias of the reverse direction of sup_eq_left.

@[simp]
theorem sup_of_le_right {α : Type u} [] {a : α} {b : α} :
a ba b = b

Alias of the reverse direction of sup_eq_right.

theorem le_of_sup_eq {α : Type u} [] {a : α} {b : α} :
a b = ba b

Alias of the forward direction of sup_eq_right.

@[simp]
theorem left_lt_sup {α : Type u} [] {a : α} {b : α} :
a < a b ¬b a
@[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 sup_idem {α : Type u} [] (a : α) :
a a = a
instance instIdempotentOpSup {α : Type u} [] :
Std.IdempotentOp fun (x x_1 : α) => x x_1
Equations
• =
theorem sup_comm {α : Type u} [] (a : α) (b : α) :
a b = b a
instance instCommutativeSup {α : Type u} [] :
Std.Commutative fun (x x_1 : α) => x x_1
Equations
• =
theorem sup_assoc {α : Type u} [] (a : α) (b : α) (c : α) :
a b c = a (b c)
instance instAssociativeSup {α : Type u} [] :
Std.Associative fun (x x_1 : α) => x x_1
Equations
• =
theorem sup_left_right_swap {α : Type u} [] (a : α) (b : α) (c : α) :
a b c = c b a
theorem sup_left_idem {α : Type u} [] (a : α) (b : α) :
a (a b) = a b
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 Ne.lt_sup_or_lt_sup {α : Type u} [] {a : α} {b : α} (hab : a b) :
a < a b b < a b
theorem Monotone.forall_le_of_antitone {α : Type u} [] {β : Type u_1} [] {f : αβ} {g : αβ} (hf : ) (hg : ) (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 SemilatticeSup.ext_sup {α : Type u_1} {A : } {B : } (H : ∀ (x y : α), x y x y) (x : α) (y : α) :
x y = x y
theorem SemilatticeSup.ext {α : Type u_1} {A : } {B : } (H : ∀ (x y : α), x y x y) :
A = B
theorem ite_le_sup {α : Type u} [] (s : α) (s' : α) (P : Prop) [] :
(if P then s else s') s s'

### Meet-semilattices #

class SemilatticeInf (α : Type u) extends , :

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.

• 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
• le_antisymm : ∀ (a b : α), a bb aa = b
• inf_le_left : ∀ (a b : α), a b a

The infimum is a lower bound on the first argument

• inf_le_right : ∀ (a b : α), a b b

The infimum is a lower bound on the second argument

• le_inf : ∀ (a b c : α), a ba ca b c

The infimum is the greatest lower bound

Instances
theorem SemilatticeInf.inf_le_left {α : Type u} [self : ] (a : α) (b : α) :
a b a

The infimum is a lower bound on the first argument

theorem SemilatticeInf.inf_le_right {α : Type u} [self : ] (a : α) (b : α) :
a b b

The infimum is a lower bound on the second argument

theorem SemilatticeInf.le_inf {α : Type u} [self : ] (a : α) (b : α) (c : α) :
a ba ca b c

The infimum is the greatest lower bound

instance OrderDual.instSemilatticeSup (α : Type u_1) [] :
Equations
instance OrderDual.instSemilatticeInf (α : Type u_1) [] :
Equations
theorem SemilatticeSup.dual_dual (α : Type u_1) [H : ] :
@[simp]
theorem inf_le_left {α : Type u} [] {a : α} {b : α} :
a b a
@[deprecated inf_le_left]
theorem inf_le_left' {α : Type u} [] {a : α} {b : α} :
a b a

Alias of inf_le_left.

@[simp]
theorem inf_le_right {α : Type u} [] {a : α} {b : α} :
a b b
@[deprecated inf_le_right]
theorem inf_le_right' {α : Type u} [] {a : α} {b : α} :
a b b

Alias of inf_le_right.

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_eq_right {α : Type u} [] {a : α} {b : α} :
a b = b b a
@[simp]
theorem left_eq_inf {α : Type u} [] {a : α} {b : α} :
a = a b a b
@[simp]
theorem right_eq_inf {α : Type u} [] {a : α} {b : α} :
b = a b b a
@[simp]
theorem inf_of_le_left {α : Type u} [] {a : α} {b : α} :
a ba b = a

Alias of the reverse direction of inf_eq_left.

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

Alias of the forward direction of inf_eq_left.

@[simp]
theorem inf_of_le_right {α : Type u} [] {a : α} {b : α} :
b aa b = b

Alias of the reverse direction of inf_eq_right.

@[simp]
theorem inf_lt_left {α : Type u} [] {a : α} {b : α} :
a b < a ¬a b
@[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_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 inf_idem {α : Type u} [] (a : α) :
a a = a
instance instIdempotentOpInf {α : Type u} [] :
Std.IdempotentOp fun (x x_1 : α) => x x_1
Equations
• =
theorem inf_comm {α : Type u} [] (a : α) (b : α) :
a b = b a
instance instCommutativeInf {α : Type u} [] :
Std.Commutative fun (x x_1 : α) => x x_1
Equations
• =
theorem inf_assoc {α : Type u} [] (a : α) (b : α) (c : α) :
a b c = a (b c)
instance instAssociativeInf {α : Type u} [] :
Std.Associative fun (x x_1 : α) => x x_1
Equations
• =
theorem inf_left_right_swap {α : Type u} [] (a : α) (b : α) (c : α) :
a b c = c b a
theorem inf_left_idem {α : Type u} [] (a : α) (b : α) :
a (a b) = a b
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 Ne.inf_lt_or_inf_lt {α : Type u} [] {a : α} {b : α} :
a ba b < a a b < b
theorem SemilatticeInf.ext_inf {α : Type u_1} {A : } {B : } (H : ∀ (x y : α), x y x y) (x : α) (y : α) :
x y = x y
theorem SemilatticeInf.ext {α : Type u_1} {A : } {B : } (H : ∀ (x y : α), x y x y) :
A = B
theorem SemilatticeInf.dual_dual (α : Type u_1) [H : ] :
theorem inf_le_ite {α : Type u} [] (s : α) (s' : α) (P : Prop) [] :
s s' if P then s else s'
def SemilatticeInf.mk' {α : Type u_1} [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
Instances For

### Lattices #

class Lattice (α : Type u) extends , :

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

• 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
• 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

The infimum is a lower bound on the first argument

• inf_le_right : ∀ (a b : α), a b b

The infimum is a lower bound on the second argument

• le_inf : ∀ (a b c : α), a ba ca b c

The infimum is the greatest lower bound

Instances
instance OrderDual.instLattice (α : Type u_1) [] :
Equations
theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder {α : Type u_1} [Sup α] [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) :
SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder

The partial orders from SemilatticeSup_mk' and SemilatticeInf_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} [Sup α] [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
• One or more equations did not get rendered due to their size.
Instances For
theorem inf_le_sup {α : Type u} [] {a : α} {b : α} :
a b a b
theorem sup_le_inf {α : Type u} [] {a : α} {b : α} :
a b a b a = b
@[simp]
theorem inf_eq_sup {α : Type u} [] {a : α} {b : α} :
a b = a b a = b
@[simp]
theorem sup_eq_inf {α : Type u} [] {a : α} {b : α} :
a b = a b a = b
@[simp]
theorem inf_lt_sup {α : Type u} [] {a : α} {b : α} :
a b < a b a b
theorem inf_eq_and_sup_eq_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a b = c a b = c a = c b = c

#### Distributivity laws #

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

### Distributive lattices #

class DistribLattice (α : Type u_1) extends :
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.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.

• 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
• 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

The infimum distributes over the supremum

Instances
theorem DistribLattice.le_sup_inf {α : Type u_1} [self : ] (x : α) (y : α) (z : α) :
(x y) (x z) x y z

The infimum distributes over the supremum

theorem le_sup_inf {α : Type u} [] {x : α} {y : α} {z : α} :
(x y) (x z) x y z
theorem sup_inf_left {α : Type u} [] (a : α) (b : α) (c : α) :
a b c = (a b) (a c)
theorem sup_inf_right {α : Type u} [] (a : α) (b : α) (c : α) :
a b c = (a c) (b c)
theorem inf_sup_left {α : Type u} [] (a : α) (b : α) (c : α) :
a (b c) = a b a c
instance OrderDual.instDistribLattice (α : Type u_1) [] :
Equations
• = let __spread.0 := ;
theorem inf_sup_right {α : Type u} [] (a : α) (b : α) (c : α) :
(a b) c = a c b c
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, inline]
abbrev DistribLattice.ofInfSupLe {α : Type u} [] (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
Instances For

### Lattices derived from linear orders #

@[instance 100]
instance LinearOrder.toLattice {α : Type u} [o : ] :
Equations
• LinearOrder.toLattice = let __spread.0 := o; Lattice.mk
theorem sup_eq_max {α : Type u} [] {a : α} {b : α} :
a b = max a b
theorem inf_eq_min {α : Type u} [] {a : α} {b : α} :
a b = min a b
theorem sup_ind {α : Type u} [] (a : α) (b : α) {p : αProp} (ha : p a) (hb : p b) :
p (a b)
@[simp]
theorem le_sup_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a b c a b a c
@[simp]
theorem lt_sup_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a < b c a < b a < c
@[simp]
theorem sup_lt_iff {α : Type u} [] {a : α} {b : α} {c : α} :
b c < a b < a c < a
theorem inf_ind {α : Type u} [] (a : α) (b : α) {p : αProp} :
p ap bp (a b)
@[simp]
theorem inf_le_iff {α : Type u} [] {a : α} {b : α} {c : α} :
b c a b a c a
@[simp]
theorem inf_lt_iff {α : Type u} [] {a : α} {b : α} {c : α} :
b c < a b < a c < a
@[simp]
theorem lt_inf_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a < b c a < b a < c
theorem max_max_max_comm {α : Type u} [] (a : α) (b : α) (c : α) (d : α) :
max (max a b) (max c d) = max (max a c) (max b d)
theorem min_min_min_comm {α : Type u} [] (a : α) (b : α) (c : α) (d : α) :
min (min a b) (min c d) = min (min a c) (min b d)
theorem sup_eq_maxDefault {α : Type u} [] [DecidableRel fun (x x_1 : α) => x x_1] [IsTotal α fun (x x_1 : α) => x x_1] :
(fun (x x_1 : α) => x x_1) = maxDefault
theorem inf_eq_minDefault {α : Type u} [] [DecidableRel fun (x x_1 : α) => x x_1] [IsTotal α fun (x x_1 : α) => x x_1] :
(fun (x x_1 : α) => x x_1) = minDefault
@[reducible, inline]
abbrev Lattice.toLinearOrder (α : Type u) [] [] [DecidableRel fun (x x_1 : α) => x x_1] [DecidableRel fun (x x_1 : α) => x < x_1] [IsTotal α fun (x x_1 : α) => x x_1] :

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations
• = let __spread.0 := inst✝³; LinearOrder.mk inst✝¹ inst✝² inst✝
Instances For
@[instance 100]
instance instDistribLatticeOfLinearOrder {α : Type u} [] :
Equations
• instDistribLatticeOfLinearOrder = let __spread.0 := ;
Equations
instance instLatticeInt :
Equations

### Dual order #

@[simp]
theorem ofDual_inf {α : Type u} [Sup α] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a b) = OrderDual.ofDual a OrderDual.ofDual b
@[simp]
theorem ofDual_sup {α : Type u} [Inf α] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (a b) = OrderDual.ofDual a OrderDual.ofDual b
@[simp]
theorem toDual_inf {α : Type u} [Inf α] (a : α) (b : α) :
OrderDual.toDual (a b) = OrderDual.toDual a OrderDual.toDual b
@[simp]
theorem toDual_sup {α : Type u} [Sup α] (a : α) (b : α) :
OrderDual.toDual (a b) = OrderDual.toDual a OrderDual.toDual b
@[simp]
theorem ofDual_min {α : Type u} [] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (min a b) = max (OrderDual.ofDual a) (OrderDual.ofDual b)
@[simp]
theorem ofDual_max {α : Type u} [] (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (max a b) = min (OrderDual.ofDual a) (OrderDual.ofDual b)
@[simp]
theorem toDual_min {α : Type u} [] (a : α) (b : α) :
OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)
@[simp]
theorem toDual_max {α : Type u} [] (a : α) (b : α) :
OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)

### Function lattices #

instance Pi.instSupForall {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Sup (α' i)] :
Sup ((i : ι) → α' i)
Equations
• Pi.instSupForall = { sup := fun (f g : (i : ι) → α' i) (i : ι) => f i g i }
@[simp]
theorem Pi.sup_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Sup (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) (i : ι) :
(f g) i = f i g i
theorem Pi.sup_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Sup (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) :
f g = fun (i : ι) => f i g i
instance Pi.instInfForall {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Inf (α' i)] :
Inf ((i : ι) → α' i)
Equations
• Pi.instInfForall = { inf := fun (f g : (i : ι) → α' i) (i : ι) => f i g i }
@[simp]
theorem Pi.inf_apply {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Inf (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) (i : ι) :
(f g) i = f i g i
theorem Pi.inf_def {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Inf (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) :
f g = fun (i : ι) => f i g i
instance Pi.instSemilatticeSup {ι : Type u_1} {α' : ιType u_2} [(i : ι) → SemilatticeSup (α' i)] :
SemilatticeSup ((i : ι) → α' i)
Equations
• Pi.instSemilatticeSup =
instance Pi.instSemilatticeInf {ι : Type u_1} {α' : ιType u_2} [(i : ι) → SemilatticeInf (α' i)] :
SemilatticeInf ((i : ι) → α' i)
Equations
• Pi.instSemilatticeInf =
instance Pi.instLattice {ι : Type u_1} {α' : ιType u_2} [(i : ι) → Lattice (α' i)] :
Lattice ((i : ι) → α' i)
Equations
instance Pi.instDistribLattice {ι : Type u_1} {α' : ιType u_2} [(i : ι) → DistribLattice (α' i)] :
DistribLattice ((i : ι) → α' i)
Equations
• Pi.instDistribLattice =
theorem Function.update_sup {ι : Type u_1} {π : ιType u_2} [] [(i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i) (i : ι) (a : π i) (b : π i) :
theorem Function.update_inf {ι : Type u_1} {π : ιType u_2} [] [(i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i) (i : ι) (a : π i) (b : π i) :

### Monotone functions and lattices #

theorem Monotone.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :

Pointwise supremum of two monotone functions is a monotone function.

theorem Monotone.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :

Pointwise infimum of two monotone functions is a monotone function.

theorem Monotone.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Monotone fun (x : α) => max (f x) (g x)

Pointwise maximum of two monotone functions is a monotone function.

theorem Monotone.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Monotone fun (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} [] [] {f : αβ} (h : ) (x : α) (y : α) :
f x f y f (x y)
theorem Monotone.map_inf_le {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (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} [] [] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem Monotone.map_inf {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem MonotoneOn.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (f g) s

Pointwise supremum of two monotone functions is a monotone function.

theorem MonotoneOn.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (f g) s

Pointwise infimum of two monotone functions is a monotone function.

theorem MonotoneOn.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (fun (x : α) => max (f x) (g x)) s

Pointwise maximum of two monotone functions is a monotone function.

theorem MonotoneOn.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
MonotoneOn (fun (x : α) => min (f x) (g x)) s

Pointwise minimum of two monotone functions is a monotone function.

theorem MonotoneOn.of_map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} [] [] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
theorem MonotoneOn.of_map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} [] [] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
theorem MonotoneOn.map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [] [] (hf : ) (hx : x s) (hy : y s) :
f (x y) = f x f y
theorem MonotoneOn.map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [] [] (hf : ) (hx : x s) (hy : y s) :
f (x y) = f x f y
theorem Antitone.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :

Pointwise supremum of two monotone functions is a monotone function.

theorem Antitone.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :

Pointwise infimum of two monotone functions is a monotone function.

theorem Antitone.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Antitone fun (x : α) => max (f x) (g x)

Pointwise maximum of two monotone functions is a monotone function.

theorem Antitone.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} (hf : ) (hg : ) :
Antitone fun (x : α) => 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 : ) (x : α) (y : α) :
f (x y) f x f y
theorem Antitone.le_map_inf {α : Type u} {β : Type v} [] [] {f : αβ} (h : ) (x : α) (y : α) :
f x f y f (x y)
theorem Antitone.map_sup {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem Antitone.map_inf {α : Type u} {β : Type v} [] [] {f : αβ} (hf : ) (x : α) (y : α) :
f (x y) = f x f y
theorem AntitoneOn.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (f g) s

Pointwise supremum of two antitone functions is an antitone function.

theorem AntitoneOn.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (f g) s

Pointwise infimum of two antitone functions is an antitone function.

theorem AntitoneOn.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (fun (x : α) => max (f x) (g x)) s

Pointwise maximum of two antitone functions is an antitone function.

theorem AntitoneOn.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {s : Set α} (hf : ) (hg : ) :
AntitoneOn (fun (x : α) => min (f x) (g x)) s

Pointwise minimum of two antitone functions is an antitone function.

theorem AntitoneOn.of_map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} [] [] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
theorem AntitoneOn.of_map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} [] [] (h : ∀ (x : α), x s∀ (y : α), y sf (x y) = f x f y) :
theorem AntitoneOn.map_sup {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [] [] (hf : ) (hx : x s) (hy : y s) :
f (x y) = f x f y
theorem AntitoneOn.map_inf {α : Type u} {β : Type v} {f : αβ} {s : Set α} {x : α} {y : α} [] [] (hf : ) (hx : x s) (hy : y s) :
f (x y) = f x f y

### Products of (semi-)lattices #

instance Prod.instSup (α : Type u) (β : Type v) [Sup α] [Sup β] :
Sup (α × β)
Equations
• = { sup := fun (p q : α × β) => (p.1 q.1, p.2 q.2) }
instance Prod.instInf (α : Type u) (β : Type v) [Inf α] [Inf β] :
Inf (α × β)
Equations
• = { inf := fun (p q : α × β) => (p.1 q.1, p.2 q.2) }
@[simp]
theorem Prod.mk_sup_mk (α : Type u) (β : Type v) [Sup α] [Sup β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
(a₁, b₁) (a₂, b₂) = (a₁ a₂, b₁ b₂)
@[simp]
theorem Prod.mk_inf_mk (α : Type u) (β : Type v) [Inf α] [Inf β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) :
(a₁, b₁) (a₂, b₂) = (a₁ a₂, b₁ b₂)
@[simp]
theorem Prod.fst_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
(p q).1 = p.1 q.1
@[simp]
theorem Prod.fst_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
(p q).1 = p.1 q.1
@[simp]
theorem Prod.snd_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
(p q).2 = p.2 q.2
@[simp]
theorem Prod.snd_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
(p q).2 = p.2 q.2
@[simp]
theorem Prod.swap_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
(p q).swap = p.swap q.swap
@[simp]
theorem Prod.swap_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
(p q).swap = p.swap q.swap
theorem Prod.sup_def (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) :
p q = (p.1 q.1, p.2 q.2)
theorem Prod.inf_def (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) :
p q = (p.1 q.1, p.2 q.2)
instance Prod.instSemilatticeSup (α : Type u) (β : Type v) [] [] :
Equations
instance Prod.instSemilatticeInf (α : Type u) (β : Type v) [] [] :
Equations
instance Prod.instLattice (α : Type u) (β : Type v) [] [] :
Lattice (α × β)
Equations
instance Prod.instDistribLattice (α : Type u) (β : Type v) [] [] :
Equations

### Subtypes of (semi-)lattices #

@[reducible, inline]
abbrev Subtype.semilatticeSup {α : Type u} [] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) :
SemilatticeSup { x : α // P x }

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

Equations
Instances For
@[reducible, inline]
abbrev Subtype.semilatticeInf {α : Type u} [] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) :
SemilatticeInf { x : α // P x }

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

Equations
Instances For
@[reducible, inline]
abbrev Subtype.lattice {α : Type u} [] {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
Instances For
@[simp]
theorem Subtype.coe_sup {α : Type u} [] {P : αProp} (Psup : ∀ ⦃x y : α⦄, P xP yP (x y)) (x : ) (y : ) :
(x y) = x y
@[simp]
theorem Subtype.coe_inf {α : Type u} [] {P : αProp} (Pinf : ∀ ⦃x y : α⦄, P xP yP (x y)) (x : ) (y : ) :
(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,
@[reducible, inline]
abbrev Function.Injective.semilatticeSup {α : Type u} {β : Type v} [Sup α] [] (f : αβ) (hf_inj : ) (map_sup : ∀ (a b : α), f (a b) = f a f b) :

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

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.semilatticeInf {α : Type u} {β : Type v} [Inf α] [] (f : αβ) (hf_inj : ) (map_inf : ∀ (a b : α), f (a b) = f a f b) :

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

Equations
Instances For
@[reducible, inline]
abbrev Function.Injective.lattice {α : Type u} {β : Type v} [Sup α] [Inf α] [] (f : αβ) (hf_inj : ) (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
• One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev Function.Injective.distribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [] (f : αβ) (hf_inj : ) (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 DistribLattice, if it admits an injective map that preserves ⊔ and ⊓ to a DistribLattice. See note [reducible non-instances].

Equations
Instances For
Equations
Equations
instance ULift.instLattice {α : Type u} [] :
Equations
Equations
instance ULift.instLinearOrder {α : Type u} [] :
Equations
Equations