mathlib docs: order.lattice

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

@[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_left_of_le {α : Type u} [semilattice_sup α] {a b c : α} :

c ≤ a → c ≤ a ⊔ b

source

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

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 : α} :

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 : α} :

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 : α} :

a ≤ b → 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 : α} :

a ⊔ b = b → a ≤ b

source

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

p a → 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 sup_idem {α : Type u} [semilattice_sup α] {a : α} :

a ⊔ a = a

source

@[instance]

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

is_idempotent α has_sup.sup

Equations

sup_is_idempotent = _

source

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

a ⊔ b = b ⊔ a

source

@[instance]

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

is_commutative α has_sup.sup

Equations

sup_is_commutative = _

source

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

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

source

@[instance]

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

is_associative α has_sup.sup

Equations

sup_is_associative = _

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

(∀ (b : α), b ≤ a) ∨ ∃ (b : α), a < 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 α} :

(∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B

source

@[class]

structure semilattice_inf :

Type u → Type u

inf : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1

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) [s : semilattice_inf α] :

partial_order α

source

@[instance]

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

has_inf α

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_left_of_le {α : Type u} [semilattice_inf α] {a b c : α} :

a ≤ c → a ⊓ b ≤ c

source

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

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 : α} :

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 : α} :

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 : α} :

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

source

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

b ≤ c → b ⊓ a ≤ c ⊓ a

source

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

b ≤ c → a ⊓ b ≤ a ⊓ c

source

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

a ⊓ b = a → a ≤ b

source

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

p a → 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_idem {α : Type u} [semilattice_inf α] {a : α} :

a ⊓ a = a

source

@[instance]

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

is_idempotent α has_inf.inf

Equations

inf_is_idempotent = _

source

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

a ⊓ b = b ⊓ a

source

@[instance]

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

is_commutative α has_inf.inf

Equations

inf_is_commutative = _

source

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

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

source

@[instance]

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

is_associative α has_inf.inf

Equations

inf_is_associative = _

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 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 α} :

(∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B

source

@[instance]

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

semilattice_sup α

source

@[instance]

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

semilattice_inf α

source

@[class]

structure lattice :

Type u → Type u

sup : α → α → α
le : α → α → Prop
lt : α → α → Prop
le_refl : ∀ (a : α), a ≤ a
le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
inf : α → α → α
inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1

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

Instances

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 lattice.ext {α : Type u_1} {A B : lattice α} :

(∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B

source

@[instance]

def distrib_lattice.to_lattice (α : Type u_1) [s : 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_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
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_1 : α), a ≤ c_1 → b ≤ c_1 → a ⊔ b ≤ c_1
inf : α → α → α
inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
le_inf : ∀ (a b c_1 : α), a ≤ b → a ≤ c_1 → a ≤ b ⊓ c_1
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 distribution properties (of sup over inf or inf over sup, on the left or right). 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

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 : α} :

x ⊓ z ≤ y ⊓ z → x ⊔ z ≤ y ⊔ z → x ≤ y

source

theorem eq_of_inf_eq_sup_eq {α : Type u} [distrib_lattice α] {a b c : α} :

b ⊓ a = c ⊓ a → b ⊔ a = c ⊔ a → b = c

source

@[instance]

def lattice_of_decidable_linear_order {α : Type u} [o : decidable_linear_order α] :

lattice α

Equations

lattice_of_decidable_linear_order = {sup := max o, le := decidable_linear_order.le o, lt := decidable_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} [decidable_linear_order α] {x y : α} :

x ⊔ y = max x y

source

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

x ⊓ y = min x y

source

@[instance]

def distrib_lattice_of_decidable_linear_order {α : Type u} [o : decidable_linear_order α] :

distrib_lattice α

Equations

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

source

@[instance]

def nat.distrib_lattice :

distrib_lattice ℕ

Equations

nat.distrib_lattice = distrib_lattice_of_decidable_linear_order

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

@[instance]

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

has_sup (order_dual α)

Equations