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

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

Join-semilattices #

source
@[class]
structure semilattice_sup (α : Type u) :
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
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 αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.has_inf (α : Type u_1) [has_sup α] :
has_inf αᵒᵈ
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 lt_sup_of_lt_left {α : Type u} [semilattice_sup α] {a b c : α} (h : c < a) :
c < a ⊔ b
source
theorem lt_sup_of_lt_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
@[simp]
theorem sup_eq_right {α : Type u} [semilattice_sup α] {a b : α} :
a ⊔ b = b ↔ a ≤ b
source
@[simp]
theorem left_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
a = a ⊔ b ↔ b ≤ a
source
@[simp]
theorem right_eq_sup {α : Type u} [semilattice_sup α] {a b : α} :
b = a ⊔ b ↔ a ≤ b
source
@[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.

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

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

source
@[simp]
theorem left_lt_sup {α : Type u} [semilattice_sup α] {a b : α} :
a < a ⊔ b ↔ ¬b ≤ a
source
@[simp]
theorem right_lt_sup {α : Type u} [semilattice_sup α] {a b : α} :
b < a ⊔ b ↔ ¬a ≤ b
source
theorem left_or_right_lt_sup {α : Type u} [semilattice_sup α] {a b : α} (h : a ≠ b) :
a < a ⊔ b ∨ b < a ⊔ b
source
theorem le_iff_exists_sup {α : Type u} [semilattice_sup α] {a b : α} :
a ≤ b ↔ ∃ (c : α), b = a ⊔ c
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
@[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 sup_sup_distrib_left {α : Type u} [semilattice_sup α] (a b c : α) :
a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)
source
theorem sup_sup_distrib_right {α : Type u} [semilattice_sup α] (a b c : α) :
a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
source
theorem sup_congr_left {α : Type u} [semilattice_sup α] {a b c : α} (hb : b ≤ a ⊔ c) (hc : c ≤ a ⊔ b) :
a ⊔ b = a ⊔ c
source
theorem sup_congr_right {α : Type u} [semilattice_sup α] {a b c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) :
a ⊔ c = b ⊔ c
source
theorem sup_eq_sup_iff_left {α : Type u} [semilattice_sup α] {a b c : α} :
a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b
source
theorem sup_eq_sup_iff_right {α : Type u} [semilattice_sup α] {a b c : α} :
a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
source
theorem ne.lt_sup_or_lt_sup {α : Type u} [semilattice_sup α] {a b : α} (hab : a ≠ b) :
a < a ⊔ b ∨ 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 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

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
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 αᵒᵈ
Equations
source
@[protected, instance]
def order_dual.semilattice_inf (α : Type u_1) [semilattice_sup α] :
semilattice_inf αᵒᵈ
Equations
source
theorem semilattice_sup.dual_dual (α : Type u_1) [H : semilattice_sup α] :
order_dual.semilattice_sup αᵒᵈ = 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
theorem inf_lt_of_left_lt {α : Type u} [semilattice_inf α] {a b c : α} (h : a < c) :
a ⊓ b < c
source
theorem inf_lt_of_right_lt {α : 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
@[simp]
theorem inf_eq_right {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b = b ↔ b ≤ a
source
@[simp]
theorem left_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
a = a ⊓ b ↔ a ≤ b
source
@[simp]
theorem right_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :
b = a ⊓ b ↔ b ≤ a
source
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.

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

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

source
@[simp]
theorem inf_lt_left {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b < a ↔ ¬a ≤ b
source
@[simp]
theorem inf_lt_right {α : Type u} [semilattice_inf α] {a b : α} :
a ⊓ b < b ↔ ¬b ≤ a
source
theorem inf_lt_left_or_right {α : Type u} [semilattice_inf α] {a b : α} (h : a ≠ b) :
a ⊓ b < a ∨ a ⊓ b < b
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
@[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 inf_inf_distrib_left {α : Type u} [semilattice_inf α] (a b c : α) :
a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c)
source
theorem inf_inf_distrib_right {α : Type u} [semilattice_inf α] (a b c : α) :
a ⊓ b ⊓ c = a ⊓ c ⊓ (b ⊓ c)
source
theorem inf_congr_left {α : Type u} [semilattice_inf α] {a b c : α} (hb : a ⊓ c ≤ b) (hc : a ⊓ b ≤ c) :
a ⊓ b = a ⊓ c
source
theorem inf_congr_right {α : Type u} [semilattice_inf α] {a b c : α} (h1 : b ⊓ c ≤ a) (h2 : a ⊓ c ≤ b) :
a ⊓ c = b ⊓ c
source
theorem inf_eq_inf_iff_left {α : Type u} [semilattice_inf α] {a b c : α} :
a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c
source
theorem inf_eq_inf_iff_right {α : Type u} [semilattice_inf α] {a b c : α} :
a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b
source
theorem ne.inf_lt_or_inf_lt {α : Type u} [semilattice_inf α] {a b : α} :
a ≠ b → a ⊓ b < a ∨ a ⊓ b < b
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 αᵒᵈ = H
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

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
source
@[protected, instance]
def order_dual.lattice (α : Type u_1) [lattice α] :
lattice αᵒᵈ
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 sup_le_inf {α : Type u} [lattice α] {a b : α} :
a ⊔ b ≤ a ⊓ b ↔ a = b
source
@[simp]
theorem inf_eq_sup {α : Type u} [lattice α] {a b : α} :
a ⊓ b = a ⊔ b ↔ a = b
source
@[simp]
theorem sup_eq_inf {α : Type u} [lattice α] {a b : α} :
a ⊔ b = a ⊓ b ↔ a = b
source
@[simp]
theorem inf_lt_sup {α : Type u} [lattice α] {a b : α} :
a ⊓ b < a ⊔ b ↔ a ≠ b
source
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 #

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 α
Instances for distrib_lattice.to_lattice
source
@[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
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 αᵒᵈ
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
source
@[reducible]
def distrib_lattice.of_inf_sup_le {α : Type u} [lattice α] (inf_sup_le : ∀ (a b c : α), a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) :
distrib_lattice α

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

Equations

Lattices derived from linear orders #

source
@[protected, instance]
def linear_order.to_lattice {α : Type u} [o : linear_order α] :
lattice α
Equations
source
theorem sup_eq_max {α : Type u} [linear_order α] {a b : α} :
a ⊔ b = linear_order.max a b
source
theorem inf_eq_min {α : Type u} [linear_order α] {a b : α} :
a ⊓ b = linear_order.min a b
source
theorem sup_ind {α : Type u} [linear_order α] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) :
p (a ⊔ b)
source
@[simp]
theorem le_sup_iff {α : Type u} [linear_order α] {a b c : α} :
a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c
source
@[simp]
theorem lt_sup_iff {α : Type u} [linear_order α] {a b c : α} :
a < b ⊔ c ↔ a < b ∨ a < c
source
@[simp]
theorem sup_lt_iff {α : Type u} [linear_order α] {a b c : α} :
b ⊔ c < a ↔ b < a ∧ c < a
source
theorem inf_ind {α : Type u} [linear_order α] (a b : α) {p : α → Prop} :
p a → p b → p (a ⊓ b)
source
@[simp]
theorem inf_le_iff {α : Type u} [linear_order α] {a b c : α} :
b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a
source
@[simp]
theorem inf_lt_iff {α : Type u} [linear_order α] {a b c : α} :
b ⊓ c < a ↔ b < a ∨ c < a
source
@[simp]
theorem lt_inf_iff {α : Type u} [linear_order α] {a b c : α} :
a < b ⊓ c ↔ a < b ∧ a < c
source
theorem max_max_max_comm {α : Type u} [linear_order α] (a b c d : α) :
linear_order.max (linear_order.max a b) (linear_order.max c d) = linear_order.max (linear_order.max a c) (linear_order.max b d)
source
theorem min_min_min_comm {α : Type u} [linear_order α] (a b c d : α) :
linear_order.min (linear_order.min a b) (linear_order.min c d) = linear_order.min (linear_order.min a c) (linear_order.min b d)
source
theorem sup_eq_max_default {α : Type u} [semilattice_sup α] [decidable_rel has_le.le] [is_total α has_le.le] :
has_sup.sup = max_default
source
theorem inf_eq_min_default {α : Type u} [semilattice_inf α] [decidable_rel has_le.le] [is_total α has_le.le] :
has_inf.inf = min_default
source
@[reducible]
def lattice.to_linear_order (α : Type u) [lattice α] [decidable_eq α] [decidable_rel has_le.le] [decidable_rel has_lt.lt] [is_total α has_le.le] :
linear_order α

A lattice with total order is a linear order.

See note [reducible non-instances].

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

Dual order #

source
@[simp]
theorem of_dual_inf {α : Type u} [has_sup α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a ⊓ b) = ⇑order_dual.of_dual a ⊔ ⇑order_dual.of_dual b
source
@[simp]
theorem of_dual_sup {α : Type u} [has_inf α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (a ⊔ b) = ⇑order_dual.of_dual a ⊓ ⇑order_dual.of_dual b
source
@[simp]
theorem to_dual_inf {α : Type u} [has_inf α] (a b : α) :
⇑order_dual.to_dual (a ⊓ b) = ⇑order_dual.to_dual a ⊔ ⇑order_dual.to_dual b
source
@[simp]
theorem to_dual_sup {α : Type u} [has_sup α] (a b : α) :
⇑order_dual.to_dual (a ⊔ b) = ⇑order_dual.to_dual a ⊓ ⇑order_dual.to_dual b
source
@[simp]
theorem of_dual_min {α : Type u} [linear_order α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (linear_order.min a b) = linear_order.max (⇑order_dual.of_dual a) (⇑order_dual.of_dual b)
source
@[simp]
theorem of_dual_max {α : Type u} [linear_order α] (a b : αᵒᵈ) :
⇑order_dual.of_dual (linear_order.max a b) = linear_order.min (⇑order_dual.of_dual a) (⇑order_dual.of_dual b)
source
@[simp]
theorem to_dual_min {α : Type u} [linear_order α] (a b : α) :
⇑order_dual.to_dual (linear_order.min a b) = linear_order.max (⇑order_dual.to_dual a) (⇑order_dual.to_dual b)
source
@[simp]
theorem to_dual_max {α : Type u} [linear_order α] (a b : α) :
⇑order_dual.to_dual (linear_order.max a b) = linear_order.min (⇑order_dual.to_dual a) (⇑order_dual.to_dual b)

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

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 : α), linear_order.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 : α), linear_order.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_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.of_map_inf {α : Type u} {β : Type v} [semilattice_inf α] [semilattice_inf β] {f : α → β} (h : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) :
monotone f
source
theorem monotone.of_map_sup {α : Type u} {β : Type v} [semilattice_sup α] [semilattice_sup β] {f : α → β} (h : ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y) :
monotone f
source
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
source
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
source
@[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) :
monotone_on (f ⊔ g) s

Pointwise supremum of two monotone functions is a monotone function.

source
@[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) :
monotone_on (f ⊓ g) s

Pointwise infimum of two monotone functions is a monotone function.

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

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

source
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) :
monotone_on f s
source
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) :
monotone_on f s
source
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
source
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
source
@[protected]
theorem antitone.sup {α : Type u} {β : Type v} [preorder α] [semilattice_sup β] {f g : α → β} (hf : antitone f) (hg : antitone g) :
antitone (f ⊔ g)

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

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

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

source
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
source
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)
source
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
source
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
source
@[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) :
antitone_on (f ⊔ g) s

Pointwise supremum of two antitone functions is a antitone function.

source
@[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) :
antitone_on (f ⊓ g) s

Pointwise infimum of two antitone functions is a antitone function.

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

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

source
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) :
antitone_on f s
source
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) :
antitone_on f s
source
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
source
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 #

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
@[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₂)
source
@[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₂)
source
@[simp]
theorem prod.fst_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
(p ⊔ q).fst = p.fst ⊔ q.fst
source
@[simp]
theorem prod.fst_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
(p ⊓ q).fst = p.fst ⊓ q.fst
source
@[simp]
theorem prod.snd_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
(p ⊔ q).snd = p.snd ⊔ q.snd
source
@[simp]
theorem prod.snd_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
(p ⊓ q).snd = p.snd ⊓ q.snd
source
@[simp]
theorem prod.swap_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
(p ⊔ q).swap = p.swap ⊔ q.swap
source
@[simp]
theorem prod.swap_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
(p ⊓ q).swap = p.swap ⊓ q.swap
source
theorem prod.sup_def (α : Type u) (β : Type v) [has_sup α] [has_sup β] (p q : α × β) :
p ⊔ q = (p.fst ⊔ q.fst, p.snd ⊔ q.snd)
source
theorem prod.inf_def (α : Type u) (β : Type v) [has_inf α] [has_inf β] (p q : α × β) :
p ⊓ q = (p.fst ⊓ q.fst, p.snd ⊓ q.snd)
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, 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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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, _⟩
source
@[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, _⟩
source
@[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) :
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, 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) :
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, 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) :
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, 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) :
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
source
@[protected, instance]
def bool.distrib_lattice  :
distrib_lattice bool
Equations