order.lattice - mathlib docs

source

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

(:a ≤ b:) → b ≤ a → a = b

source

@[class]

structure has_sup (α : Type u) :

Type u

sup : α → α → α

Typeclass for the ⊔ (\lub) notation

Instances

source

@[class]

structure has_inf (α : Type u) :

Type u

inf : α → α → α

Typeclass for the ⊓ (\glb) notation

Instances

source

@[class]

structure semilattice_sup (α : Type u) :

Type u

sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c

A semilattice_sup is a join-semilattice, that is, a partial order with a join (a.k.a. lub / least upper bound, sup / supremum) operation ⊔ which is the least element larger than both factors.

Instances

source

@[instance]

def semilattice_sup.to_has_sup (α : Type u) [self : semilattice_sup α] :

has_sup α

source

@[instance]

def semilattice_sup.to_partial_order (α : Type u) [self : semilattice_sup α] :

partial_order α

source

def semilattice_sup.mk' {α : Type u_1} [has_sup α] (sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a) (sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (sup_idem : ∀ (a : α), a ⊔ a = a) :

semilattice_sup α

A type with a commutative, associative and idempotent binary sup operation has the structure of a join-semilattice.

The partial order is defined so that a ≤ b unfolds to a ⊔ b = b; cf. sup_eq_right.

Equations

semilattice_sup.mk' sup_comm sup_assoc sup_idem = {sup := has_sup.sup _inst_1, le := λ (a b : α), a ⊔ b = b, lt := partial_order.lt._default (λ (a b : α), a ⊔ b = b), le_refl := sup_idem, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

def order_dual.has_sup (α : Type u_1) [has_inf α] :

has_sup (order_dual α)

Equations

order_dual.has_sup α = {sup := has_inf.inf _inst_1}

source

@[protected, instance]

def order_dual.has_inf (α : Type u_1) [has_sup α] :

has_inf (order_dual α)

Equations

order_dual.has_inf α = {inf := has_sup.sup _inst_1}

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

theorem sup_of_le_left {α : Type u} [semilattice_sup α] {a b : α} (h : b ≤ a) :

a ⊔ b = a

source

@[simp]

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

a = a ⊔ b ↔ b ≤ a

source

@[simp]

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

a ⊔ b = b ↔ a ≤ b

source

theorem sup_of_le_right {α : Type u} [semilattice_sup α] {a b : α} (h : a ≤ b) :

a ⊔ b = b

source

@[simp]

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

b = a ⊔ b ↔ a ≤ b

source

theorem sup_le_sup {α : Type u} [semilattice_sup α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

a ⊔ c ≤ b ⊔ d

source

theorem sup_le_sup_left {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a ≤ b) (c : α) :

c ⊔ a ≤ c ⊔ b

source

theorem sup_le_sup_right {α : Type u} [semilattice_sup α] {a b : α} (h₁ : a ≤ b) (c : α) :

a ⊔ c ≤ b ⊔ c

source

theorem le_of_sup_eq {α : Type u} [semilattice_sup α] {a b : α} (h : a ⊔ b = b) :

a ≤ b

source

theorem sup_ind {α : Type u} [semilattice_sup α] [is_total α has_le.le] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) :

p (a ⊔ b)

source

@[simp]

theorem sup_lt_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :

b ⊔ c < a ↔ b < a ∧ c < a

source

@[simp]

theorem le_sup_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :

a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

source

@[simp]

theorem lt_sup_iff {α : Type u} [semilattice_sup α] [is_total α has_le.le] {a b c : α} :

a < b ⊔ c ↔ a < b ∨ a < c

source

@[simp]

theorem sup_idem {α : Type u} [semilattice_sup α] {a : α} :

a ⊔ a = a

source

@[protected, instance]

def sup_is_idempotent {α : Type u} [semilattice_sup α] :

is_idempotent α has_sup.sup

source

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

a ⊔ b = b ⊔ a

source

@[protected, instance]

def sup_is_commutative {α : Type u} [semilattice_sup α] :

is_commutative α has_sup.sup

source

theorem sup_assoc {α : Type u} [semilattice_sup α] {a b c : α} :

a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

source

@[protected, instance]

def sup_is_associative {α : Type u} [semilattice_sup α] :

is_associative α has_sup.sup

source

theorem sup_left_right_swap {α : Type u} [semilattice_sup α] (a b c : α) :

a ⊔ b ⊔ c = c ⊔ b ⊔ a

source

@[simp]

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

a ⊔ (a ⊔ b) = a ⊔ b

source

@[simp]

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

a ⊔ b ⊔ b = a ⊔ b

source

theorem sup_left_comm {α : Type u} [semilattice_sup α] (a b c : α) :

a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

source

theorem sup_right_comm {α : Type u} [semilattice_sup α] (a b c : α) :

a ⊔ b ⊔ c = a ⊔ c ⊔ b

source

theorem sup_sup_sup_comm {α : Type u} [semilattice_sup α] (a b c d : α) :

a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

source

theorem 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 forall_le_or_exists_lt_sup {α : Type u} [semilattice_sup α] (a : α) :

(∀ (b : α), b ≤ a) ∨ ∃ (b : α), a < b

source

theorem monotone.forall_le_of_antitone {α : Type u} [semilattice_sup α] {β : Type u_1} [preorder β] {f g : α → β} (hf : monotone f) (hg : antitone g) (h : f ≤ g) (m n : α) :

f m ≤ g n

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

source

theorem semilattice_sup.ext_sup {α : Type u_1} {A B : semilattice_sup α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) (x y : α) :

x ⊔ y = x ⊔ y

source

theorem semilattice_sup.ext {α : Type u_1} {A B : semilattice_sup α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

source

theorem exists_lt_of_sup (α : Type u_1) [semilattice_sup α] [nontrivial α] :

∃ (a b : α), a < b

source

theorem ite_le_sup {α : Type u} [semilattice_sup α] (s s' : α) (P : Prop) [decidable P] :

ite P s s' ≤ s ⊔ s'

source

@[instance]

def semilattice_inf.to_has_inf (α : Type u) [self : semilattice_inf α] :

has_inf α

source

@[class]

structure semilattice_inf (α : Type u) :

Type u

inf : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c

A semilattice_inf is a meet-semilattice, that is, a partial order with a meet (a.k.a. glb / greatest lower bound, inf / infimum) operation ⊓ which is the greatest element smaller than both factors.

Instances

source

@[instance]

def semilattice_inf.to_partial_order (α : Type u) [self : semilattice_inf α] :

partial_order α

source

@[protected, instance]

def order_dual.semilattice_sup (α : Type u_1) [semilattice_inf α] :

semilattice_sup (order_dual α)

Equations

order_dual.semilattice_sup α = {sup := has_sup.sup (order_dual.has_sup α), le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

def order_dual.semilattice_inf (α : Type u_1) [semilattice_sup α] :

semilattice_inf (order_dual α)

Equations

order_dual.semilattice_inf α = {inf := has_inf.inf (order_dual.has_inf α), le := partial_order.le (order_dual.partial_order α), lt := partial_order.lt (order_dual.partial_order α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

theorem semilattice_sup.dual_dual (α : Type u_1) [H : semilattice_sup α] :

order_dual.semilattice_sup (order_dual α) = H

source

@[simp]

theorem inf_le_left {α : Type u} [semilattice_inf α] {a b : α} :

a ⊓ b ≤ a

source

theorem inf_le_left' {α : Type u} [semilattice_inf α] {a b : α} :

(:a ⊓ b:) ≤ a

source

@[simp]

theorem inf_le_right {α : Type u} [semilattice_inf α] {a b : α} :

a ⊓ b ≤ b

source

theorem inf_le_right' {α : Type u} [semilattice_inf α] {a b : α} :

(:a ⊓ b:) ≤ b

source

theorem le_inf {α : Type u} [semilattice_inf α] {a b c : α} :

a ≤ b → a ≤ c → a ≤ b ⊓ c

source

theorem inf_le_of_left_le {α : Type u} [semilattice_inf α] {a b c : α} (h : a ≤ c) :

a ⊓ b ≤ c

source

theorem inf_le_of_right_le {α : Type u} [semilattice_inf α] {a b c : α} (h : b ≤ c) :

a ⊓ b ≤ c

source

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

theorem inf_of_le_left {α : Type u} [semilattice_inf α] {a b : α} (h : a ≤ b) :

a ⊓ b = a

source

@[simp]

theorem left_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :

a = a ⊓ b ↔ a ≤ b

source

@[simp]

theorem inf_eq_right {α : Type u} [semilattice_inf α] {a b : α} :

a ⊓ b = b ↔ b ≤ a

source

theorem inf_of_le_right {α : Type u} [semilattice_inf α] {a b : α} (h : b ≤ a) :

a ⊓ b = b

source

@[simp]

theorem right_eq_inf {α : Type u} [semilattice_inf α] {a b : α} :

b = a ⊓ b ↔ b ≤ a

source

theorem inf_le_inf {α : Type u} [semilattice_inf α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :

a ⊓ c ≤ b ⊓ d

source

theorem inf_le_inf_right {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b ≤ c) :

b ⊓ a ≤ c ⊓ a

source

theorem inf_le_inf_left {α : Type u} [semilattice_inf α] (a : α) {b c : α} (h : b ≤ c) :

a ⊓ b ≤ a ⊓ c

source

theorem le_of_inf_eq {α : Type u} [semilattice_inf α] {a b : α} (h : a ⊓ b = a) :

a ≤ b

source

theorem inf_ind {α : Type u} [semilattice_inf α] [is_total α has_le.le] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) :

p (a ⊓ b)

source

@[simp]

theorem lt_inf_iff {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b c : α} :

a < b ⊓ c ↔ a < b ∧ a < c

source

@[simp]

theorem inf_le_iff {α : Type u} [semilattice_inf α] [is_total α has_le.le] {a b c : α} :

b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a

source

@[simp]

theorem inf_idem {α : Type u} [semilattice_inf α] {a : α} :

a ⊓ a = a

source

@[protected, instance]

def inf_is_idempotent {α : Type u} [semilattice_inf α] :

is_idempotent α has_inf.inf

source

theorem inf_comm {α : Type u} [semilattice_inf α] {a b : α} :

a ⊓ b = b ⊓ a

source

@[protected, instance]

def inf_is_commutative {α : Type u} [semilattice_inf α] :

is_commutative α has_inf.inf

source

theorem inf_assoc {α : Type u} [semilattice_inf α] {a b c : α} :

a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

source

@[protected, instance]

def inf_is_associative {α : Type u} [semilattice_inf α] :

is_associative α has_inf.inf

source

theorem inf_left_right_swap {α : Type u} [semilattice_inf α] (a b c : α) :

a ⊓ b ⊓ c = c ⊓ b ⊓ a

source

@[simp]

theorem inf_left_idem {α : Type u} [semilattice_inf α] {a b : α} :

a ⊓ (a ⊓ b) = a ⊓ b

source

@[simp]

theorem inf_right_idem {α : Type u} [semilattice_inf α] {a b : α} :

a ⊓ b ⊓ b = a ⊓ b

source

theorem inf_left_comm {α : Type u} [semilattice_inf α] (a b c : α) :

a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)

source

theorem inf_right_comm {α : Type u} [semilattice_inf α] (a b c : α) :

a ⊓ b ⊓ c = a ⊓ c ⊓ b

source

theorem inf_inf_inf_comm {α : Type u} [semilattice_inf α] (a b c d : α) :

a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)

source

theorem 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 forall_le_or_exists_lt_inf {α : Type u} [semilattice_inf α] (a : α) :

(∀ (b : α), a ≤ b) ∨ ∃ (b : α), b < a

source

theorem semilattice_inf.ext_inf {α : Type u_1} {A B : semilattice_inf α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) (x y : α) :

x ⊓ y = x ⊓ y

source

theorem semilattice_inf.ext {α : Type u_1} {A B : semilattice_inf α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) :

A = B

source

theorem semilattice_inf.dual_dual (α : Type u_1) [H : semilattice_inf α] :

order_dual.semilattice_inf (order_dual α) = H

source

theorem exists_lt_of_inf (α : Type u_1) [semilattice_inf α] [nontrivial α] :

∃ (a b : α), a < b

source

theorem inf_le_ite {α : Type u} [semilattice_inf α] (s s' : α) (P : Prop) [decidable P] :

s ⊓ s' ≤ ite P s s'

source

def semilattice_inf.mk' {α : Type u_1} [has_inf α] (inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a) (inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ (a : α), a ⊓ a = a) :

semilattice_inf α

A type with a commutative, associative and idempotent binary inf operation has the structure of a meet-semilattice.

The partial order is defined so that a ≤ b unfolds to b ⊓ a = a; cf. inf_eq_right.

Equations

semilattice_inf.mk' inf_comm inf_assoc inf_idem = order_dual.semilattice_inf (order_dual α)

source

@[instance]

def lattice.to_semilattice_inf (α : Type u) [self : lattice α] :

semilattice_inf α

source

@[instance]

def lattice.to_semilattice_sup (α : Type u) [self : lattice α] :

semilattice_sup α

source

@[class]

structure lattice (α : Type u) :

Type u

sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
inf : α → α → α
inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c

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

Instances

source

@[protected, instance]

def order_dual.lattice (α : Type u_1) [lattice α] :

lattice (order_dual α)

Equations

order_dual.lattice α = {sup := semilattice_sup.sup (order_dual.semilattice_sup α), le := semilattice_sup.le (order_dual.semilattice_sup α), lt := semilattice_sup.lt (order_dual.semilattice_sup α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf (order_dual.semilattice_inf α), inf_le_left := _, inf_le_right := _, le_inf := _}

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

lattice.mk' sup_comm sup_assoc inf_comm inf_assoc sup_inf_self inf_sup_self = have sup_idem : ∀ (b : α), b ⊔ b = b, from _, have inf_idem : ∀ (b : α), b ⊓ b = b, from _, let semilatt_inf_inst : semilattice_inf α := semilattice_inf.mk' inf_comm inf_assoc inf_idem, semilatt_sup_inst : semilattice_sup α := semilattice_sup.mk' sup_comm sup_assoc sup_idem, partial_order_inst : partial_order α := semilattice_sup.to_partial_order α in have partial_order_eq : partial_order_inst = semilattice_inf.to_partial_order α, from _, {sup := semilattice_sup.sup semilatt_sup_inst, le := partial_order.le partial_order_inst, lt := partial_order.lt partial_order_inst, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf semilatt_inf_inst, inf_le_left := _, inf_le_right := _, le_inf := _}

source

theorem inf_le_sup {α : Type u} [lattice α] {a b : α} :

a ⊓ b ≤ a ⊔ b

source

@[simp]

theorem inf_lt_sup {α : Type u} [lattice α] {a b : α} :

a ⊓ b < a ⊔ b ↔ a ≠ b

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

source

@[instance]

def distrib_lattice.to_lattice (α : Type u_1) [self : distrib_lattice α] :

lattice α

source

@[class]

structure distrib_lattice (α : Type u_1) :

Type u_1

sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
inf : α → α → α
inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

A distributive lattice is a lattice that satisfies any of four equivalent distributive properties (of sup over inf or inf over sup, on the left or right).

The definition here chooses le_sup_inf: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z).

A classic example of a distributive lattice is the lattice of subsets of a set, and in fact this example is generic in the sense that every distributive lattice is realizable as a sublattice of a powerset lattice.

Instances

source

theorem le_sup_inf {α : Type u} [distrib_lattice α] {x y z : α} :

(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

source

theorem sup_inf_left {α : Type u} [distrib_lattice α] {x y z : α} :

x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)

source

theorem sup_inf_right {α : Type u} [distrib_lattice α] {x y z : α} :

y ⊓ z ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)

source

theorem inf_sup_left {α : Type u} [distrib_lattice α] {x y z : α} :

x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z

source

@[protected, instance]

def order_dual.distrib_lattice (α : Type u_1) [distrib_lattice α] :

distrib_lattice (order_dual α)

Equations

order_dual.distrib_lattice α = {sup := lattice.sup (order_dual.lattice α), le := lattice.le (order_dual.lattice α), lt := lattice.lt (order_dual.lattice α), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (order_dual.lattice α), inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

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

@[protected, instance]

def linear_order.to_lattice {α : Type u} [o : linear_order α] :

lattice α

Equations

linear_order.to_lattice = {sup := max o, le := linear_order.le o, lt := linear_order.lt o, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := min o, inf_le_left := _, inf_le_right := _, le_inf := _}

source

theorem sup_eq_max {α : Type u} [linear_order α] {x y : α} :

x ⊔ y = max x y

source

theorem inf_eq_min {α : Type u} [linear_order α] {x y : α} :

x ⊓ y = min x y

source

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

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

lattice.to_linear_order α = {le := lattice.le _inst_1, lt := lattice.lt _inst_1, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := _inst_3, decidable_eq := _inst_2, decidable_lt := _inst_4, max := has_sup.sup (semilattice_sup.to_has_sup α), max_def := _, min := has_inf.inf (semilattice_inf.to_has_inf α), min_def := _}

source

@[protected, instance]

def linear_order.to_distrib_lattice {α : Type u} [o : linear_order α] :

distrib_lattice α

Equations

linear_order.to_distrib_lattice = {sup := lattice.sup linear_order.to_lattice, le := lattice.le linear_order.to_lattice, lt := lattice.lt linear_order.to_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf linear_order.to_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected, instance]

def nat.distrib_lattice :

distrib_lattice ℕ

Equations

nat.distrib_lattice = linear_order.to_distrib_lattice

source

@[protected, instance]

def pi.has_sup {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), has_sup (α' i)] :

has_sup (Π (i : ι), α' i)

Equations

pi.has_sup = {sup := λ (f g : Π (i : ι), α' i) (i : ι), f i ⊔ g i}

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

pi.has_inf = {inf := λ (f g : Π (i : ι), α' i) (i : ι), f i ⊓ g i}

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

pi.semilattice_sup = {sup := has_sup.sup pi.has_sup, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

def pi.semilattice_inf {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), semilattice_inf (α' i)] :

semilattice_inf (Π (i : ι), α' i)

Equations

pi.semilattice_inf = {inf := has_inf.inf pi.has_inf, le := partial_order.le pi.partial_order, lt := partial_order.lt pi.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def pi.lattice {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), lattice (α' i)] :

lattice (Π (i : ι), α' i)

Equations

pi.lattice = {sup := semilattice_sup.sup pi.semilattice_sup, le := semilattice_sup.le pi.semilattice_sup, lt := semilattice_sup.lt pi.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf pi.semilattice_inf, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def pi.distrib_lattice {ι : Type u_1} {α' : ι → Type u_2} [Π (i : ι), distrib_lattice (α' i)] :

distrib_lattice (Π (i : ι), α' i)

Equations

pi.distrib_lattice = {sup := lattice.sup pi.lattice, le := lattice.le pi.lattice, lt := lattice.lt pi.lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf pi.lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected]

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

monotone (f ⊔ g)

Pointwise supremum of two monotone functions is a monotone function.

source

@[protected]

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

monotone (f ⊓ g)

Pointwise infimum of two monotone functions is a monotone function.

source

@[protected]

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

monotone (λ (x : α), max (f x) (g x))

Pointwise maximum of two monotone functions is a monotone function.

source

@[protected]

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

monotone (λ (x : α), min (f x) (g x))

Pointwise minimum of two monotone functions is a monotone function.

source

theorem monotone.le_map_sup {α : Type u} {β : Type v} [semilattice_sup α] [semilattice_sup β] {f : α → β} (h : monotone f) (x y : α) :

f x ⊔ f y ≤ f (x ⊔ y)

source

theorem monotone.map_sup {α : Type u} {β : Type v} [semilattice_sup α] [is_total α has_le.le] [semilattice_sup β] {f : α → β} (hf : monotone f) (x y : α) :

f (x ⊔ y) = f x ⊔ f y

source

theorem monotone.map_inf_le {α : Type u} {β : Type v} [semilattice_inf α] [semilattice_inf β] {f : α → β} (h : monotone f) (x y : α) :

f (x ⊓ y) ≤ f x ⊓ f y

source

theorem monotone.map_inf {α : Type u} {β : Type v} [semilattice_inf α] [is_total α has_le.le] [semilattice_inf β] {f : α → β} (hf : monotone f) (x y : α) :

f (x ⊓ y) = f x ⊓ f y

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 : α), 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 : α), 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.map_sup {α : Type u} {β : Type v} [semilattice_sup α] [is_total α has_le.le] [semilattice_inf β] {f : α → β} (hf : 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_inf {α : Type u} {β : Type v} [semilattice_inf α] [is_total α has_le.le] [semilattice_sup β] {f : α → β} (hf : antitone f) (x y : α) :

f (x ⊓ y) = f x ⊔ f y

source

@[protected, instance]

def prod.has_sup (α : Type u) (β : Type v) [has_sup α] [has_sup β] :

has_sup (α × β)

Equations

prod.has_sup α β = {sup := λ (p q : α × β), (p.fst ⊔ q.fst, p.snd ⊔ q.snd)}

source

@[protected, instance]

def prod.has_inf (α : Type u) (β : Type v) [has_inf α] [has_inf β] :

has_inf (α × β)

Equations

prod.has_inf α β = {inf := λ (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

prod.semilattice_sup α β = {sup := has_sup.sup (prod.has_sup α β), le := partial_order.le (prod.partial_order α β), lt := partial_order.lt (prod.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected, instance]

def prod.semilattice_inf (α : Type u) (β : Type v) [semilattice_inf α] [semilattice_inf β] :

semilattice_inf (α × β)

Equations

prod.semilattice_inf α β = {inf := has_inf.inf (prod.has_inf α β), le := partial_order.le (prod.partial_order α β), lt := partial_order.lt (prod.partial_order α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def prod.lattice (α : Type u) (β : Type v) [lattice α] [lattice β] :

lattice (α × β)

Equations

prod.lattice α β = {sup := semilattice_sup.sup (prod.semilattice_sup α β), le := semilattice_inf.le (prod.semilattice_inf α β), lt := semilattice_inf.lt (prod.semilattice_inf α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf (prod.semilattice_inf α β), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected, instance]

def prod.distrib_lattice (α : Type u) (β : Type v) [distrib_lattice α] [distrib_lattice β] :

distrib_lattice (α × β)

Equations

prod.distrib_lattice α β = {sup := lattice.sup (prod.lattice α β), le := lattice.le (prod.lattice α β), lt := lattice.lt (prod.lattice α β), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := lattice.inf (prod.lattice α β), inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

source

@[protected]

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

semilattice_sup {x // P x}

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

Equations

subtype.semilattice_sup Psup = {sup := λ (x y : {x // P x}), ⟨x.val ⊔ y.val, _⟩, le := partial_order.le (subtype.partial_order P), lt := partial_order.lt (subtype.partial_order P), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected]

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

semilattice_inf {x // P x}

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

Equations

subtype.semilattice_inf Pinf = {inf := λ (x y : {x // P x}), ⟨x.val ⊓ y.val, _⟩, le := partial_order.le (subtype.partial_order P), lt := partial_order.lt (subtype.partial_order P), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected]

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

lattice {x // P x}

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

Equations

subtype.lattice Psup Pinf = {sup := semilattice_sup.sup (subtype.semilattice_sup Psup), le := semilattice_inf.le (subtype.semilattice_inf Pinf), lt := semilattice_inf.lt (subtype.semilattice_inf Pinf), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf (subtype.semilattice_inf Pinf), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected]

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

semilattice_sup α

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

Equations

function.injective.semilattice_sup f hf_inj map_sup = {sup := has_sup.sup _inst_1, le := partial_order.le (partial_order.lift f hf_inj), lt := partial_order.lt (partial_order.lift f hf_inj), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

source

@[protected]

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

semilattice_inf α

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

Equations

function.injective.semilattice_inf f hf_inj map_inf = {inf := has_inf.inf _inst_1, le := partial_order.le (partial_order.lift f hf_inj), lt := partial_order.lt (partial_order.lift f hf_inj), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected]

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

lattice α

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

Equations

function.injective.lattice f hf_inj map_sup map_inf = {sup := semilattice_sup.sup (function.injective.semilattice_sup f hf_inj map_sup), le := semilattice_sup.le (function.injective.semilattice_sup f hf_inj map_sup), lt := semilattice_sup.lt (function.injective.semilattice_sup f hf_inj map_sup), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := semilattice_inf.inf (function.injective.semilattice_inf f hf_inj map_inf), inf_le_left := _, inf_le_right := _, le_inf := _}

source

@[protected]

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

distrib_lattice α

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

Equations