mathlib3 documentation

order.lattice

(Semi-)lattices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Semilattices are partially ordered sets with join (greatest lower bound, or sup) or meet (least upper bound, or inf) operations. Lattices are posets that are both join-semilattices and meet-semilattices.

Distributive lattices are lattices which satisfy any of four equivalent distributivity properties, of sup over inf, on the left or on the right.

Main declarations #

Notations #

TODO #

Tags #

semilattice, lattice

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

Join-semilattices #

@[class]
structure semilattice_sup (α : Type u) :

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.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} [semilattice_sup α] {a b : α} :
a a b
theorem le_sup_left' {α : Type u} [semilattice_sup α] {a b : α} :
a (:a b:)
@[simp]
theorem le_sup_right {α : Type u} [semilattice_sup α] {a b : α} :
b a b
theorem le_sup_right' {α : Type u} [semilattice_sup α] {a b : α} :
b (:a b:)
theorem le_sup_of_le_left {α : Type u} [semilattice_sup α] {a b c : α} (h : c a) :
c a b
theorem le_sup_of_le_right {α : Type u} [semilattice_sup α] {a b c : α} (h : c b) :
c a b
theorem lt_sup_of_lt_left {α : Type u} [semilattice_sup α] {a b c : α} (h : c < a) :
c < a b
theorem lt_sup_of_lt_right {α : Type u} [semilattice_sup α] {a b c : α} (h : c < b) :
c < a b
theorem sup_le {α : Type u} [semilattice_sup α] {a b c : α} :
a c b c a 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
@[simp]
theorem sup_eq_right {α : Type u} [semilattice_sup α] {a b : α} :
a b = b a b
@[simp]
theorem left_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
a = a b b a
@[simp]
theorem right_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
b = a b a b
@[simp]
theorem sup_of_le_left {α : Type u} [semilattice_sup α] {a b : α} :
b a a b = a

Alias of the reverse direction of sup_eq_left.

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

Alias of the reverse direction of sup_eq_right.

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

Alias of the forward direction of sup_eq_right.

@[simp]
theorem left_lt_sup {α : Type u} [semilattice_sup α] {a b : α} :
a < a b ¬b a
@[simp]
theorem right_lt_sup {α : Type u} [semilattice_sup α] {a b : α} :
b < a b ¬a b
theorem left_or_right_lt_sup {α : Type u} [semilattice_sup α] {a b : α} (h : a b) :
a < a b b < a b
theorem le_iff_exists_sup {α : Type u} [semilattice_sup α] {a b : α} :
a b (c : α), b = a c
theorem sup_le_sup {α : Type u} [semilattice_sup α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
a c b d
theorem sup_le_sup_left {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a b) (c : α) :
c a c b
theorem sup_le_sup_right {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a b) (c : α) :
a c b c
@[simp]
theorem sup_idem {α : Type u} [semilattice_sup α] {a : α} :
a a = a
@[protected, instance]
theorem sup_comm {α : Type u} [semilattice_sup α] {a b : α} :
a b = b a
@[protected, instance]
theorem sup_assoc {α : Type u} [semilattice_sup α] {a b c : α} :
a b c = a (b c)
@[protected, instance]
theorem sup_left_right_swap {α : Type u} [semilattice_sup α] (a b c : α) :
a b c = c b a
@[simp]
theorem sup_left_idem {α : Type u} [semilattice_sup α] {a b : α} :
a (a b) = a b
@[simp]
theorem sup_right_idem {α : Type u} [semilattice_sup α] {a b : α} :
a b b = a b
theorem sup_left_comm {α : Type u} [semilattice_sup α] (a b c : α) :
a (b c) = b (a c)
theorem sup_right_comm {α : Type u} [semilattice_sup α] (a b c : α) :
a b c = a c b
theorem sup_sup_sup_comm {α : Type u} [semilattice_sup α] (a b c d : α) :
a b (c d) = a c (b d)
theorem sup_sup_distrib_left {α : Type u} [semilattice_sup α] (a b c : α) :
a (b c) = a b (a c)
theorem sup_sup_distrib_right {α : Type u} [semilattice_sup α] (a b c : α) :
a b c = a c (b c)
theorem sup_congr_left {α : Type u} [semilattice_sup α] {a b c : α} (hb : b a c) (hc : c a b) :
a b = a c
theorem sup_congr_right {α : Type u} [semilattice_sup α] {a b c : α} (ha : a b c) (hb : b a c) :
a c = b c
theorem sup_eq_sup_iff_left {α : Type u} [semilattice_sup α] {a b c : α} :
a b = a c b a c c a b
theorem sup_eq_sup_iff_right {α : Type u} [semilattice_sup α] {a b c : α} :
a c = b c a b c b a c
theorem ne.lt_sup_or_lt_sup {α : Type u} [semilattice_sup α] {a b : α} (hab : a b) :
a < a b b < a b
theorem monotone.forall_le_of_antitone {α : Type u} [semilattice_sup α] {β : Type u_1} [preorder β] {f g : α β} (hf : monotone f) (hg : antitone g) (h : f g) (m n : α) :
f m g n

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

theorem semilattice_sup.ext_sup {α : Type u_1} {A B : semilattice_sup α} (H : (x y : α), x y x y) (x y : α) :
x y = x y
theorem semilattice_sup.ext {α : Type u_1} {A B : semilattice_sup α} (H : (x y : α), x y x y) :
A = B
theorem ite_le_sup {α : Type u} [semilattice_sup α] (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) :

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]
@[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 b a c a b c
theorem inf_le_of_left_le {α : Type u} [semilattice_inf α] {a b c : α} (h : a c) :
a b c
theorem inf_le_of_right_le {α : Type u} [semilattice_inf α] {a b c : α} (h : b c) :
a b c
theorem inf_lt_of_left_lt {α : Type u} [semilattice_inf α] {a b c : α} (h : a < c) :
a b < c
theorem inf_lt_of_right_lt {α : Type u} [semilattice_inf α] {a b c : α} (h : b < c) :
a b < c
@[simp]
theorem le_inf_iff {α : Type u} [semilattice_inf α] {a b c : α} :
a b c a b a c
@[simp]
theorem inf_eq_left {α : Type u} [semilattice_inf α] {a b : α} :
a b = a a b
@[simp]
theorem inf_eq_right {α : Type u} [semilattice_inf α] {a b : α} :
a b = b b a
@[simp]
theorem left_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
a = a b a b
@[simp]
theorem right_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
b = a b b a
theorem le_of_inf_eq {α : Type u} [semilattice_inf α] {a b : α} :
a b = a a b

Alias of the forward direction of inf_eq_left.

@[simp]
theorem inf_of_le_left {α : Type u} [semilattice_inf α] {a b : α} :
a b a b = a

Alias of the reverse direction of inf_eq_left.

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

Alias of the reverse direction of inf_eq_right.

@[simp]
theorem inf_lt_left {α : Type u} [semilattice_inf α] {a b : α} :
a b < a ¬a b
@[simp]
theorem inf_lt_right {α : Type u} [semilattice_inf α] {a b : α} :
a b < b ¬b a
theorem inf_lt_left_or_right {α : Type u} [semilattice_inf α] {a b : α} (h : a b) :
a b < a a b < b
theorem inf_le_inf {α : Type u} [semilattice_inf α] {a b c d : α} (h₁ : a b) (h₂ : c d) :
a c b d
theorem inf_le_inf_right {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b c) :
b a c a
theorem inf_le_inf_left {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b c) :
a b a c
@[simp]
theorem inf_idem {α : Type u} [semilattice_inf α] {a : α} :
a a = a
@[protected, instance]
theorem inf_comm {α : Type u} [semilattice_inf α] {a b : α} :
a b = b a
@[protected, instance]
theorem inf_assoc {α : Type u} [semilattice_inf α] {a b c : α} :
a b c = a (b c)
@[protected, instance]
theorem inf_left_right_swap {α : Type u} [semilattice_inf α] (a b c : α) :
a b c = c b a
@[simp]
theorem inf_left_idem {α : Type u} [semilattice_inf α] {a b : α} :
a (a b) = a b
@[simp]
theorem inf_right_idem {α : Type u} [semilattice_inf α] {a b : α} :
a b b = a b
theorem inf_left_comm {α : Type u} [semilattice_inf α] (a b c : α) :
a (b c) = b (a c)
theorem inf_right_comm {α : Type u} [semilattice_inf α] (a b c : α) :
a b c = a c b
theorem inf_inf_inf_comm {α : Type u} [semilattice_inf α] (a b c d : α) :
a b (c d) = a c (b d)
theorem inf_inf_distrib_left {α : Type u} [semilattice_inf α] (a b c : α) :
a (b c) = a b (a c)
theorem inf_inf_distrib_right {α : Type u} [semilattice_inf α] (a b c : α) :
a b c = a c (b c)
theorem inf_congr_left {α : Type u} [semilattice_inf α] {a b c : α} (hb : a c b) (hc : a b c) :
a b = a c
theorem inf_congr_right {α : Type u} [semilattice_inf α] {a b c : α} (h1 : b c a) (h2 : a c b) :
a c = b c
theorem inf_eq_inf_iff_left {α : Type u} [semilattice_inf α] {a b c : α} :
a b = a c a c b a b c
theorem inf_eq_inf_iff_right {α : Type u} [semilattice_inf α] {a b c : α} :
a c = b c b c a a c b
theorem ne.inf_lt_or_inf_lt {α : Type u} [semilattice_inf α] {a b : α} :
a b a b < a a b < 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 inf_le_ite {α : Type u} [semilattice_inf α] (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) :

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
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 sup_le_inf {α : Type u} [lattice α] {a b : α} :
a b a b a = b
@[simp]
theorem inf_eq_sup {α : Type u} [lattice α] {a b : α} :
a b = a b a = b
@[simp]
theorem sup_eq_inf {α : Type u} [lattice α] {a b : α} :
a b = a b a = b
@[simp]
theorem inf_lt_sup {α : Type u} [lattice α] {a b : α} :
a b < a b a b
theorem inf_eq_and_sup_eq_iff {α : Type u} [lattice α] {a b c : α} :
a b = c a b = c a = c b = c

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

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} [distrib_lattice α] {x y z : α} :
(x y) (x z) x y z
theorem sup_inf_left {α : Type u} [distrib_lattice α] {x y z : α} :
x y z = (x y) (x z)
theorem sup_inf_right {α : Type u} [distrib_lattice α] {x y z : α} :
y z x = (y x) (z x)
theorem inf_sup_left {α : Type u} [distrib_lattice α] {x y z : α} :
x (y z) = x y x z
theorem inf_sup_right {α : Type u} [distrib_lattice α] {x y z : α} :
(y z) x = y x z x
theorem le_of_inf_le_sup_le {α : Type u} [distrib_lattice α] {x y z : α} (h₁ : x z y z) (h₂ : x z y z) :
x y
theorem eq_of_inf_eq_sup_eq {α : Type u} [distrib_lattice α] {a b c : α} (h₁ : b a = c a) (h₂ : b a = c a) :
b = c
@[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 : α} :
theorem inf_eq_min {α : Type u} [linear_order α] {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 a p b p (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
@[reducible]

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations

Dual order #

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
theorem function.update_sup {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), semilattice_sup (π i)] (f : Π (i : ι), π i) (i : ι) (a b : π i) :
theorem function.update_inf {ι : Type u_1} {π : ι Type u_2} [decidable_eq ι] [Π (i : ι), semilattice_inf (π i)] (f : Π (i : ι), π i) (i : ι) (a b : π i) :

Monotone functions and lattices #

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

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

@[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} [semilattice_sup α] [semilattice_sup β] {f : α β} (h : monotone f) (x y : α) :
f x f y f (x 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.of_map_inf {α : Type u} {β : Type v} [semilattice_inf α] [semilattice_inf β] {f : α β} (h : (x y : α), f (x y) = f x f y) :
theorem monotone.of_map_sup {α : Type u} {β : Type v} [semilattice_sup α] [semilattice_sup β] {f : α β} (h : (x y : α), f (x y) = f x f y) :
theorem monotone.map_sup {α : Type u} {β : Type v} [linear_order α] [semilattice_sup β] {f : α β} (hf : monotone f) (x y : α) :
f (x y) = f x f y
theorem monotone.map_inf {α : Type u} {β : Type v} [linear_order α] [semilattice_inf β] {f : α β} (hf : monotone f) (x y : α) :
f (x y) = f x f y
@[protected]
theorem monotone_on.sup {α : Type u} {β : Type v} [preorder α] [semilattice_sup β] {f g : α β} {s : set α} (hf : monotone_on f s) (hg : monotone_on g s) :

Pointwise supremum of two monotone functions is a monotone function.

@[protected]
theorem monotone_on.inf {α : Type u} {β : Type v} [preorder α] [semilattice_inf β] {f g : α β} {s : set α} (hf : monotone_on f s) (hg : monotone_on g 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 : monotone_on f s) (hg : monotone_on g 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 : monotone_on f s) (hg : monotone_on g s) :
monotone_on (λ (x : α), linear_order.min (f x) (g x)) s

Pointwise minimum of two monotone functions is a monotone function.

theorem monotone_on.of_map_inf {α : Type u} {β : Type v} {f : α β} {s : set α} [semilattice_inf α] [semilattice_inf β] (h : (x : α), x s (y : α), y s f (x y) = f x f y) :
theorem monotone_on.of_map_sup {α : Type u} {β : Type v} {f : α β} {s : set α} [semilattice_sup α] [semilattice_sup β] (h : (x : α), x s (y : α), y s f (x y) = f x f y) :
theorem monotone_on.map_sup {α : Type u} {β : Type v} {f : α β} {s : set α} {x y : α} [linear_order α] [semilattice_sup β] (hf : monotone_on f s) (hx : x s) (hy : y s) :
f (x y) = f x f y
theorem monotone_on.map_inf {α : Type u} {β : Type v} {f : α β} {s : set α} {x y : α} [linear_order α] [semilattice_inf β] (hf : monotone_on f s) (hx : x s) (hy : y s) :
f (x y) = f x f y
@[protected]
theorem antitone.sup {α : Type u} {β : Type v} [preorder α] [semilattice_sup β] {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 α] [semilattice_inf β] {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} [semilattice_sup α] [semilattice_inf β] {f : α β} (h : antitone f) (x y : α) :
f (x y) f x f y
theorem antitone.le_map_inf {α : Type u} {β : Type v} [semilattice_inf α] [semilattice_sup β] {f : α β} (h : antitone f) (x y : α) :
f x f y f (x y)
theorem antitone.map_sup {α : Type u} {β : Type v} [linear_order α] [semilattice_inf β] {f : α β} (hf : antitone f) (x y : α) :
f (x y) = f x f y
theorem antitone.map_inf {α : Type u} {β : Type v} [linear_order α] [semilattice_sup β] {f : α β} (hf : antitone f) (x y : α) :
f (x y) = f x f y
@[protected]
theorem antitone_on.sup {α : Type u} {β : Type v} [preorder α] [semilattice_sup β] {f g : α β} {s : set α} (hf : antitone_on f s) (hg : antitone_on g s) :

Pointwise supremum of two antitone functions is a antitone function.

@[protected]
theorem antitone_on.inf {α : Type u} {β : Type v} [preorder α] [semilattice_inf β] {f g : α β} {s : set α} (hf : antitone_on f s) (hg : antitone_on g 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 : antitone_on f s) (hg : antitone_on g 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 : antitone_on f s) (hg : antitone_on g s) :
antitone_on (λ (x : α), linear_order.min (f x) (g x)) s

Pointwise minimum of two antitone functions is a antitone function.

theorem antitone_on.of_map_inf {α : Type u} {β : Type v} {f : α β} {s : set α} [semilattice_inf α] [semilattice_sup β] (h : (x : α), x s (y : α), y s f (x y) = f x f y) :
theorem antitone_on.of_map_sup {α : Type u} {β : Type v} {f : α β} {s : set α} [semilattice_sup α] [semilattice_inf β] (h : (x : α), x s (y : α), y s f (x y) = f x f y) :
theorem antitone_on.map_sup {α : Type u} {β : Type v} {f : α β} {s : set α} {x y : α} [linear_order α] [semilattice_inf β] (hf : antitone_on f s) (hx : x s) (hy : y s) :
f (x y) = f x f y
theorem antitone_on.map_inf {α : Type u} {β : Type v} {f : α β} {s : set α} {x y : α} [linear_order α] [semilattice_sup β] (hf : antitone_on f s) (hx : x s) (hy : y s) :
f (x y) = f x f y

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
@[simp]
theorem prod.mk_sup_mk (α : Type u) (β : Type v) [has_sup α] [has_sup β] (a₁ a₂ : α) (b₁ b₂ : β) :
(a₁, b₁) (a₂, b₂) = (a₁ a₂, b₁ b₂)
@[simp]
theorem prod.mk_inf_mk (α : Type u) (β : Type v) [has_inf α] [has_inf β] (a₁ a₂ : α) (b₁ b₂ : β) :
(a₁, b₁) (a₂, b₂) = (a₁ a₂, b₁ b₂)
@[simp]
theorem prod.fst_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
(p q).fst = p.fst q.fst
@[simp]
theorem prod.fst_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
(p q).fst = p.fst q.fst
@[simp]
theorem prod.snd_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
(p q).snd = p.snd q.snd
@[simp]
theorem prod.snd_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
(p q).snd = p.snd q.snd
@[simp]
theorem prod.swap_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
(p q).swap = p.swap q.swap
@[simp]
theorem prod.swap_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
(p q).swap = p.swap q.swap
theorem prod.sup_def (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
p q = (p.fst q.fst, p.snd q.snd)
theorem prod.inf_def (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
p q = (p.fst q.fst, p.snd q.snd)
@[protected, instance]
def prod.semilattice_sup (α : Type u) (β : Type v) [semilattice_sup α] [semilattice_sup β] :
Equations
@[protected, instance]
def prod.semilattice_inf (α : Type u) (β : Type v) [semilattice_inf α] [semilattice_inf β] :
Equations
@[protected, instance]
def prod.lattice (α : Type u) (β : Type v) [lattice α] [lattice β] :
lattice × β)
Equations
@[protected, instance]
def prod.distrib_lattice (α : Type u) (β : Type v) [distrib_lattice α] [distrib_lattice β] :
Equations

Subtypes of (semi-)lattices #

@[protected, reducible]
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
@[protected, reducible]
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
@[protected, reducible]
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
@[simp, norm_cast]
theorem subtype.coe_sup {α : Type u} [semilattice_sup α] {P : α Prop} (Psup : ⦃x y : α⦄, P x P y P (x y)) (x y : subtype P) :
(x y) = x y
@[simp, norm_cast]
theorem subtype.coe_inf {α : Type u} [semilattice_inf α] {P : α Prop} (Pinf : ⦃x y : α⦄, P x P y P (x y)) (x y : subtype P) :
(x y) = x y
@[simp]
theorem subtype.mk_sup_mk {α : Type u} [semilattice_sup α] {P : α Prop} (Psup : ⦃x y : α⦄, P x P y P (x y)) {x y : α} (hx : P x) (hy : P y) :
x, hx⟩ y, hy⟩ = x y, _⟩
@[simp]
theorem subtype.mk_inf_mk {α : Type u} [semilattice_inf α] {P : α Prop} (Pinf : ⦃x y : α⦄, P x P y P (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 α] [semilattice_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 α] [semilattice_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 α] [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) :

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