(Semi-)lattices

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

• SemilatticeSup: a type class for join semilattices

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

• SemilatticeInf: a type class for meet semilattices

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

• Lattice: a type class for lattices

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

• DistribLattice: a type class for distributive lattices.

Notations

• a ⊔ b: the supremum or join of a and b
• a ⊓ b: the infimum or meet of a and b

TODO

• (Semi-)lattice homomorphisms
• Alternative constructors for distributive lattices from the other distributive properties

Tags

semilattice, lattice

Join-semilattices

class SemilatticeSup (α : Type u) extends Sup , PartialOrder : Type u

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

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

  The supremum is an upper bound on the first argument

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

  The supremum is an upper bound on the second argument

• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c

  The supremum is the least upper bound

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

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

• One or more equations did not get rendered due to their size.

instance instSupOrderDual (α : Type u_1) [Inf α] : Sup αᵒᵈ

Equations

• instSupOrderDual α = { sup := fun (x x_1 : α) => x ⊓ x_1 }

instance instInfOrderDual (α : Type u_1) [Sup α] : Inf αᵒᵈ

Equations

• instInfOrderDual α = { inf := fun (x x_1 : α) => x ⊔ x_1 }

@[simp]

theorem le_sup_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ≤ a ⊔ b

theorem le_sup_left' {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ≤ a ⊔ b

@[simp]

theorem le_sup_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} : b ≤ a ⊔ b

theorem le_sup_right' {α : Type u} [SemilatticeSup α] {a : α} {b : α} : b ≤ a ⊔ b

theorem le_sup_of_le_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c ≤ a) : c ≤ a ⊔ b

theorem le_sup_of_le_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c ≤ b) : c ≤ a ⊔ b

theorem lt_sup_of_lt_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c < a) : c < a ⊔ b

theorem lt_sup_of_lt_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (h : c < b) : c < a ⊔ b

theorem sup_le {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} : a ≤ c → b ≤ c → a ⊔ b ≤ c

@[simp]

theorem sup_le_iff {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} : a ⊔ b ≤ c ↔ a ≤ c ∧ b ≤ c

@[simp]

theorem sup_eq_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ⊔ b = a ↔ b ≤ a

@[simp]

theorem sup_eq_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ⊔ b = b ↔ a ≤ b

@[simp]

theorem left_eq_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a = a ⊔ b ↔ b ≤ a

@[simp]

theorem right_eq_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} : b = a ⊔ b ↔ a ≤ b

@[simp]

theorem sup_of_le_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} : b ≤ a → a ⊔ b = a

Alias of the reverse direction of sup_eq_left.

theorem le_of_sup_eq {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ⊔ b = b → a ≤ b

Alias of the forward direction of sup_eq_right.

@[simp]

theorem sup_of_le_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ≤ b → a ⊔ b = b

Alias of the reverse direction of sup_eq_right.

@[simp]

theorem left_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a < a ⊔ b ↔ ¬b ≤ a

@[simp]

theorem right_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} : b < a ⊔ b ↔ ¬a ≤ b

theorem left_or_right_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} (h : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b

theorem le_iff_exists_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ≤ b ↔ ∃ (c : α), b = a ⊔ c

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

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

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

theorem sup_idem {α : Type u} [SemilatticeSup α] {a : α} : a ⊔ a = a

instance instIdempotentOpSupToSup {α : Type u} [SemilatticeSup α] : Std.IdempotentOp fun (x x_1 : α) => x ⊔ x_1

Equations

• (_ : Std.IdempotentOp fun (x x_1 : α) => x ⊔ x_1) = (_ : Std.IdempotentOp fun (x x_1 : α) => x ⊔ x_1)

theorem sup_comm {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ⊔ b = b ⊔ a

instance instCommutativeSupToSup {α : Type u} [SemilatticeSup α] : Std.Commutative fun (x x_1 : α) => x ⊔ x_1

Equations

• (_ : Std.Commutative fun (x x_1 : α) => x ⊔ x_1) = (_ : Std.Commutative fun (x x_1 : α) => x ⊔ x_1)

theorem sup_assoc {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} : a ⊔ b ⊔ c = a ⊔ (b ⊔ c)

instance instAssociativeSupToSup {α : Type u} [SemilatticeSup α] : Std.Associative fun (x x_1 : α) => x ⊔ x_1

Equations

• (_ : Std.Associative fun (x x_1 : α) => x ⊔ x_1) = (_ : Std.Associative fun (x x_1 : α) => x ⊔ x_1)

theorem sup_left_right_swap {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) : a ⊔ b ⊔ c = c ⊔ b ⊔ a

theorem sup_left_idem {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ⊔ (a ⊔ b) = a ⊔ b

theorem sup_right_idem {α : Type u} [SemilatticeSup α] {a : α} {b : α} : a ⊔ b ⊔ b = a ⊔ b

theorem sup_left_comm {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) : a ⊔ (b ⊔ c) = b ⊔ (a ⊔ c)

theorem sup_right_comm {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ b

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

theorem sup_sup_distrib_left {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) : a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

theorem sup_sup_distrib_right {α : Type u} [SemilatticeSup α] (a : α) (b : α) (c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

theorem sup_congr_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (hb : b ≤ a ⊔ c) (hc : c ≤ a ⊔ b) : a ⊔ b = a ⊔ c

theorem sup_congr_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} (ha : a ≤ b ⊔ c) (hb : b ≤ a ⊔ c) : a ⊔ c = b ⊔ c

theorem sup_eq_sup_iff_left {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} : a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b

theorem sup_eq_sup_iff_right {α : Type u} [SemilatticeSup α] {a : α} {b : α} {c : α} : a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

theorem Ne.lt_sup_or_lt_sup {α : Type u} [SemilatticeSup α] {a : α} {b : α} (hab : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b

theorem Monotone.forall_le_of_antitone {α : Type u} [SemilatticeSup α] {β : 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 SemilatticeSup.ext_sup {α : Type u_1} {A : SemilatticeSup α} {B : SemilatticeSup α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) (x : α) (y : α) : x ⊔ y = x ⊔ y

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

theorem ite_le_sup {α : Type u} [SemilatticeSup α] (s : α) (s' : α) (P : Prop) [Decidable P] : (if P then s else s') ≤ s ⊔ s'

Meet-semilattices

class SemilatticeInf (α : Type u) extends Inf , PartialOrder : Type u

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

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

  The infimum is a lower bound on the first argument

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

  The infimum is a lower bound on the second argument

• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c

  The infimum is the greatest lower bound

instance OrderDual.semilatticeSup (α : Type u_1) [SemilatticeInf α] : SemilatticeSup αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

instance OrderDual.semilatticeInf (α : Type u_1) [SemilatticeSup α] : SemilatticeInf αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

theorem SemilatticeSup.dual_dual (α : Type u_1) [H : SemilatticeSup α] : OrderDual.semilatticeSup αᵒᵈ = H

@[simp]

theorem inf_le_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b ≤ a

theorem inf_le_left' {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b ≤ a

@[simp]

theorem inf_le_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b ≤ b

theorem inf_le_right' {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b ≤ b

theorem le_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} : a ≤ b → a ≤ c → a ≤ b ⊓ c

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

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

theorem inf_lt_of_left_lt {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h : a < c) : a ⊓ b < c

theorem inf_lt_of_right_lt {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h : b < c) : a ⊓ b < c

@[simp]

theorem le_inf_iff {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} : a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c

@[simp]

theorem inf_eq_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b = a ↔ a ≤ b

@[simp]

theorem inf_eq_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b = b ↔ b ≤ a

@[simp]

theorem left_eq_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a = a ⊓ b ↔ a ≤ b

@[simp]

theorem right_eq_inf {α : Type u} [SemilatticeInf α] {a : α} {b : α} : b = a ⊓ b ↔ b ≤ a

@[simp]

theorem inf_of_le_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ≤ b → a ⊓ b = a

Alias of the reverse direction of inf_eq_left.

theorem le_of_inf_eq {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b = a → a ≤ b

Alias of the forward direction of inf_eq_left.

@[simp]

theorem inf_of_le_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} : b ≤ a → a ⊓ b = b

Alias of the reverse direction of inf_eq_right.

@[simp]

theorem inf_lt_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b < a ↔ ¬a ≤ b

@[simp]

theorem inf_lt_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b < b ↔ ¬b ≤ a

theorem inf_lt_left_or_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} (h : a ≠ b) : a ⊓ b < a ∨ a ⊓ b < b

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

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

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

theorem inf_idem {α : Type u} [SemilatticeInf α] {a : α} : a ⊓ a = a

instance instIdempotentOpInfToInf {α : Type u} [SemilatticeInf α] : Std.IdempotentOp fun (x x_1 : α) => x ⊓ x_1

Equations

• (_ : Std.IdempotentOp fun (x x_1 : α) => x ⊓ x_1) = (_ : Std.IdempotentOp fun (x x_1 : α) => x ⊓ x_1)

theorem inf_comm {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b = b ⊓ a

instance instCommutativeInfToInf {α : Type u} [SemilatticeInf α] : Std.Commutative fun (x x_1 : α) => x ⊓ x_1

Equations

• (_ : Std.Commutative fun (x x_1 : α) => x ⊓ x_1) = (_ : Std.Commutative fun (x x_1 : α) => x ⊓ x_1)

theorem inf_assoc {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} : a ⊓ b ⊓ c = a ⊓ (b ⊓ c)

instance instAssociativeInfToInf {α : Type u} [SemilatticeInf α] : Std.Associative fun (x x_1 : α) => x ⊓ x_1

Equations

• (_ : Std.Associative fun (x x_1 : α) => x ⊓ x_1) = (_ : Std.Associative fun (x x_1 : α) => x ⊓ x_1)

theorem inf_left_right_swap {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) : a ⊓ b ⊓ c = c ⊓ b ⊓ a

theorem inf_left_idem {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ (a ⊓ b) = a ⊓ b

theorem inf_right_idem {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ⊓ b ⊓ b = a ⊓ b

theorem inf_left_comm {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c)

theorem inf_right_comm {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ b

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

theorem inf_inf_distrib_left {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) : a ⊓ (b ⊓ c) = a ⊓ b ⊓ (a ⊓ c)

theorem inf_inf_distrib_right {α : Type u} [SemilatticeInf α] (a : α) (b : α) (c : α) : a ⊓ b ⊓ c = a ⊓ c ⊓ (b ⊓ c)

theorem inf_congr_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (hb : a ⊓ c ≤ b) (hc : a ⊓ b ≤ c) : a ⊓ b = a ⊓ c

theorem inf_congr_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} (h1 : b ⊓ c ≤ a) (h2 : a ⊓ c ≤ b) : a ⊓ c = b ⊓ c

theorem inf_eq_inf_iff_left {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} : a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c

theorem inf_eq_inf_iff_right {α : Type u} [SemilatticeInf α] {a : α} {b : α} {c : α} : a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b

theorem Ne.inf_lt_or_inf_lt {α : Type u} [SemilatticeInf α] {a : α} {b : α} : a ≠ b → a ⊓ b < a ∨ a ⊓ b < b

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

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

theorem SemilatticeInf.dual_dual (α : Type u_1) [H : SemilatticeInf α] : OrderDual.semilatticeInf αᵒᵈ = H

theorem inf_le_ite {α : Type u} [SemilatticeInf α] (s : α) (s' : α) (P : Prop) [Decidable P] : s ⊓ s' ≤ if P then s else s'

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

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

• SemilatticeInf.mk' inf_comm inf_assoc inf_idem = OrderDual.semilatticeInf αᵒᵈ

Lattices

class Lattice (α : Type u) extends SemilatticeSup , Inf : Type u

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

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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

  The infimum is a lower bound on the first argument

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

  The infimum is a lower bound on the second argument

• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c

  The infimum is the greatest lower bound

instance OrderDual.lattice (α : Type u_1) [Lattice α] : Lattice αᵒᵈ

Equations

• One or more equations did not get rendered due to their size.

theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder {α : Type u_1} [Sup α] [Inf α] (sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a) (sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (sup_idem : ∀ (a : α), a ⊔ a = a) (inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a) (inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (inf_idem : ∀ (a : α), a ⊓ a = a) (sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a) (inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a) : SemilatticeSup.toPartialOrder = SemilatticeInf.toPartialOrder

The partial orders from SemilatticeSup_mk' and SemilatticeInf_mk' agree if sup and inf satisfy the lattice absorption laws sup_inf_self (a ⊔ a ⊓ b = a) and inf_sup_self (a ⊓ (a ⊔ b) = a).

def Lattice.mk' {α : Type u_1} [Sup α] [Inf α] (sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a) (sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)) (inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a) (inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)) (sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a) (inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a) : 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

• One or more equations did not get rendered due to their size.

theorem inf_le_sup {α : Type u} [Lattice α] {a : α} {b : α} : a ⊓ b ≤ a ⊔ b

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 : Lattice α} {B : Lattice α} (H : ∀ (x y : α), x ≤ y ↔ x ≤ y) : A = B

Distributive lattices

class DistribLattice (α : Type u_1) extends Lattice : Type u_1

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

The definition here chooses le_sup_inf: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z). To prove distributivity from the dual law, use DistribLattice.of_inf_sup_le.

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

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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

  The infimum distributes over the supremum

theorem le_sup_inf {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} : (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

theorem sup_inf_left {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} : x ⊔ y ⊓ z = (x ⊔ y) ⊓ (x ⊔ z)

theorem sup_inf_right {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} : y ⊓ z ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)

theorem inf_sup_left {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} : x ⊓ (y ⊔ z) = x ⊓ y ⊔ x ⊓ z

instance OrderDual.distribLattice (α : Type u_1) [DistribLattice α] : DistribLattice αᵒᵈ

Equations

• OrderDual.distribLattice α = let src := inferInstanceAs (Lattice αᵒᵈ); DistribLattice.mk (_ : ∀ (x x_1 x_2 : αᵒᵈ), (x ⊔ x_1) ⊓ (x ⊔ x_2) ≤ x ⊔ x_1 ⊓ x_2)

theorem inf_sup_right {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} : (y ⊔ z) ⊓ x = y ⊓ x ⊔ z ⊓ x

theorem le_of_inf_le_sup_le {α : Type u} [DistribLattice α] {x : α} {y : α} {z : α} (h₁ : x ⊓ z ≤ y ⊓ z) (h₂ : x ⊔ z ≤ y ⊔ z) : x ≤ y

theorem eq_of_inf_eq_sup_eq {α : Type u} [DistribLattice α] {a : α} {b : α} {c : α} (h₁ : b ⊓ a = c ⊓ a) (h₂ : b ⊔ a = c ⊔ a) : b = c

@[reducible]

def DistribLattice.ofInfSupLe {α : Type u} [Lattice α] (inf_sup_le : ∀ (a b c : α), a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c) : DistribLattice α

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

Equations

• DistribLattice.ofInfSupLe inf_sup_le = DistribLattice.mk (_ : ∀ (x y z : αᵒᵈᵒᵈ), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)

Lattices derived from linear orders

instance LinearOrder.toLattice {α : Type u} [o : LinearOrder α] : Lattice α

Equations

• LinearOrder.toLattice = Lattice.mk (_ : ∀ (a b : α), min a b ≤ a) (_ : ∀ (a b : α), min a b ≤ b) (_ : ∀ (x x_1 x_2 : α), x ≤ x_1 → x ≤ x_2 → x ≤ min x_1 x_2)

theorem sup_eq_max {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊔ b = max a b

theorem inf_eq_min {α : Type u} [LinearOrder α] {a : α} {b : α} : a ⊓ b = min a b

theorem sup_ind {α : Type u} [LinearOrder α] (a : α) (b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊔ b)

@[simp]

theorem le_sup_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

@[simp]

theorem lt_sup_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a < b ⊔ c ↔ a < b ∨ a < c

@[simp]

theorem sup_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : b ⊔ c < a ↔ b < a ∧ c < a

theorem inf_ind {α : Type u} [LinearOrder α] (a : α) (b : α) {p : α → Prop} : p a → p b → p (a ⊓ b)

@[simp]

theorem inf_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a

@[simp]

theorem inf_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : b ⊓ c < a ↔ b < a ∨ c < a

@[simp]

theorem lt_inf_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} : a < b ⊓ c ↔ a < b ∧ a < c

theorem max_max_max_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) (d : α) : max (max a b) (max c d) = max (max a c) (max b d)

theorem min_min_min_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) (d : α) : min (min a b) (min c d) = min (min a c) (min b d)

theorem sup_eq_maxDefault {α : Type u} [SemilatticeSup α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] [IsTotal α fun (x x_1 : α) => x ≤ x_1] : (fun (x x_1 : α) => x ⊔ x_1) = maxDefault

theorem inf_eq_minDefault {α : Type u} [SemilatticeInf α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] [IsTotal α fun (x x_1 : α) => x ≤ x_1] : (fun (x x_1 : α) => x ⊓ x_1) = minDefault

@[reducible]

def Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α] [DecidableRel fun (x x_1 : α) => x ≤ x_1] [DecidableRel fun (x x_1 : α) => x < x_1] [IsTotal α fun (x x_1 : α) => x ≤ x_1] : LinearOrder α

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations

• Lattice.toLinearOrder α = let src := inst✝³; LinearOrder.mk (_ : ∀ (a b : α), a ≤ b ∨ b ≤ a) inst✝¹ inst✝² inst✝

instance instDistribLattice {α : Type u} [LinearOrder α] : DistribLattice α

Equations

• instDistribLattice = let src := inferInstanceAs (Lattice α); DistribLattice.mk (_ : ∀ (x b c : α), (x ⊔ b) ⊓ (x ⊔ c) ≤ x ⊔ b ⊓ c)

instance instDistribLatticeNat : DistribLattice ℕ

Equations

• instDistribLatticeNat = inferInstance

instance instLatticeInt : Lattice ℤ

Equations

• instLatticeInt = inferInstance

Dual order

@[simp]

theorem ofDual_inf {α : Type u} [Sup α] (a : αᵒᵈ) (b : αᵒᵈ) : OrderDual.ofDual (a ⊓ b) = OrderDual.ofDual a ⊔ OrderDual.ofDual b

@[simp]

theorem ofDual_sup {α : Type u} [Inf α] (a : αᵒᵈ) (b : αᵒᵈ) : OrderDual.ofDual (a ⊔ b) = OrderDual.ofDual a ⊓ OrderDual.ofDual b

@[simp]

theorem toDual_inf {α : Type u} [Inf α] (a : α) (b : α) : OrderDual.toDual (a ⊓ b) = OrderDual.toDual a ⊔ OrderDual.toDual b

@[simp]

theorem toDual_sup {α : Type u} [Sup α] (a : α) (b : α) : OrderDual.toDual (a ⊔ b) = OrderDual.toDual a ⊓ OrderDual.toDual b

@[simp]

theorem ofDual_min {α : Type u} [LinearOrder α] (a : αᵒᵈ) (b : αᵒᵈ) : OrderDual.ofDual (min a b) = max (OrderDual.ofDual a) (OrderDual.ofDual b)

@[simp]

theorem ofDual_max {α : Type u} [LinearOrder α] (a : αᵒᵈ) (b : αᵒᵈ) : OrderDual.ofDual (max a b) = min (OrderDual.ofDual a) (OrderDual.ofDual b)

@[simp]

theorem toDual_min {α : Type u} [LinearOrder α] (a : α) (b : α) : OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)

@[simp]

theorem toDual_max {α : Type u} [LinearOrder α] (a : α) (b : α) : OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)

Function lattices

instance Pi.instSupForAll {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Sup (α' i)] : Sup ((i : ι) → α' i)

Equations

• Pi.instSupForAll = { sup := fun (f g : (i : ι) → α' i) (i : ι) => f i ⊔ g i }

@[simp]

theorem Pi.sup_apply {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Sup (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) (i : ι) : (f ⊔ g) i = f i ⊔ g i

theorem Pi.sup_def {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Sup (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) : f ⊔ g = fun (i : ι) => f i ⊔ g i

instance Pi.instInfForAll {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Inf (α' i)] : Inf ((i : ι) → α' i)

Equations

• Pi.instInfForAll = { inf := fun (f g : (i : ι) → α' i) (i : ι) => f i ⊓ g i }

@[simp]

theorem Pi.inf_apply {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Inf (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) (i : ι) : (f ⊓ g) i = f i ⊓ g i

theorem Pi.inf_def {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Inf (α' i)] (f : (i : ι) → α' i) (g : (i : ι) → α' i) : f ⊓ g = fun (i : ι) => f i ⊓ g i

instance Pi.semilatticeSup {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → SemilatticeSup (α' i)] : SemilatticeSup ((i : ι) → α' i)

Equations

• One or more equations did not get rendered due to their size.

instance Pi.semilatticeInf {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → SemilatticeInf (α' i)] : SemilatticeInf ((i : ι) → α' i)

Equations

• One or more equations did not get rendered due to their size.

instance Pi.lattice {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Lattice (α' i)] : Lattice ((i : ι) → α' i)

Equations

• One or more equations did not get rendered due to their size.

instance Pi.distribLattice {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → DistribLattice (α' i)] : DistribLattice ((i : ι) → α' i)

Equations

• Pi.distribLattice = DistribLattice.mk (_ : ∀ (x x_1 x_2 : (i : ι) → α' i) (x_3 : ι), (x x_3 ⊔ x_1 x_3) ⊓ (x x_3 ⊔ x_2 x_3) ≤ x x_3 ⊔ x_1 x_3 ⊓ x_2 x_3)

theorem Function.update_sup {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i) (i : ι) (a : π i) (b : π i) : Function.update f i (a ⊔ b) = Function.update f i a ⊔ Function.update f i b

theorem Function.update_inf {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → SemilatticeInf (π i)] (f : (i : ι) → π i) (i : ι) (a : π i) (b : π i) : Function.update f i (a ⊓ b) = Function.update f i a ⊓ Function.update f i b

Monotone functions and lattices

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

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

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

Pointwise maximum of two monotone functions is a monotone function.

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

Pointwise minimum of two monotone functions is a monotone function.

theorem Monotone.le_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : Monotone f) (x : α) (y : α) : f x ⊔ f y ≤ f (x ⊔ y)

theorem Monotone.map_inf_le {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : Monotone f) (x : α) (y : α) : f (x ⊓ y) ≤ f x ⊓ f y

theorem Monotone.of_map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeInf β] {f : α → β} (h : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y) : Monotone f

theorem Monotone.of_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ (x y : α), f (x ⊔ y) = f x ⊔ f y) : Monotone f

theorem Monotone.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : α → β} (hf : Monotone f) (x : α) (y : α) : f (x ⊔ y) = f x ⊔ f y

theorem Monotone.map_inf {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeInf β] {f : α → β} (hf : Monotone f) (x : α) (y : α) : f (x ⊓ y) = f x ⊓ f y

theorem MonotoneOn.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : α → β} {g : α → β} {s : Set α} (hf : MonotoneOn f s) (hg : MonotoneOn g s) : MonotoneOn (f ⊔ g) s

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

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

Pointwise maximum of two monotone functions is a monotone function.

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

Pointwise minimum of two monotone functions is a monotone function.

theorem MonotoneOn.of_map_inf {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeInf α] [SemilatticeInf β] (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊓ f y) : MonotoneOn f s

theorem MonotoneOn.of_map_sup {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeSup α] [SemilatticeSup β] (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊔ f y) : MonotoneOn f s

theorem MonotoneOn.map_sup {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊔ y) = f x ⊔ f y

theorem MonotoneOn.map_inf {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeInf β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊓ y) = f x ⊓ f y

theorem Antitone.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : α → β} {g : α → β} (hf : Antitone f) (hg : Antitone g) : Antitone (f ⊔ g)

Pointwise supremum of two monotone functions is a monotone function.

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

Pointwise infimum of two monotone functions is a monotone function.

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

Pointwise maximum of two monotone functions is a monotone function.

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

Pointwise minimum of two monotone functions is a monotone function.

theorem Antitone.map_sup_le {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeInf β] {f : α → β} (h : Antitone f) (x : α) (y : α) : f (x ⊔ y) ≤ f x ⊓ f y

theorem Antitone.le_map_inf {α : Type u} {β : Type v} [SemilatticeInf α] [SemilatticeSup β] {f : α → β} (h : Antitone f) (x : α) (y : α) : f x ⊔ f y ≤ f (x ⊓ y)

theorem Antitone.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeInf β] {f : α → β} (hf : Antitone f) (x : α) (y : α) : f (x ⊔ y) = f x ⊓ f y

theorem Antitone.map_inf {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : α → β} (hf : Antitone f) (x : α) (y : α) : f (x ⊓ y) = f x ⊔ f y

theorem AntitoneOn.sup {α : Type u} {β : Type v} [Preorder α] [SemilatticeSup β] {f : α → β} {g : α → β} {s : Set α} (hf : AntitoneOn f s) (hg : AntitoneOn g s) : AntitoneOn (f ⊔ g) s

Pointwise supremum of two antitone functions is an antitone function.

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

Pointwise infimum of two antitone functions is an antitone function.

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

Pointwise maximum of two antitone functions is an antitone function.

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

Pointwise minimum of two antitone functions is an antitone function.

theorem AntitoneOn.of_map_inf {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeInf α] [SemilatticeSup β] (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y) : AntitoneOn f s

theorem AntitoneOn.of_map_sup {α : Type u} {β : Type v} {f : α → β} {s : Set α} [SemilatticeSup α] [SemilatticeInf β] (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊔ y) = f x ⊓ f y) : AntitoneOn f s

theorem AntitoneOn.map_sup {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeInf β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊔ y) = f x ⊓ f y

theorem AntitoneOn.map_inf {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x : α} {y : α} [LinearOrder α] [SemilatticeSup β] (hf : AntitoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (x ⊓ y) = f x ⊔ f y

Products of (semi-)lattices

instance Prod.instSupProd (α : Type u) (β : Type v) [Sup α] [Sup β] : Sup (α × β)

Equations

• Prod.instSupProd α β = { sup := fun (p q : α × β) => (p.1 ⊔ q.1, p.2 ⊔ q.2) }

instance Prod.instInfProd (α : Type u) (β : Type v) [Inf α] [Inf β] : Inf (α × β)

Equations

• Prod.instInfProd α β = { inf := fun (p q : α × β) => (p.1 ⊓ q.1, p.2 ⊓ q.2) }

@[simp]

theorem Prod.mk_sup_mk (α : Type u) (β : Type v) [Sup α] [Sup β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) : (a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂)

@[simp]

theorem Prod.mk_inf_mk (α : Type u) (β : Type v) [Inf α] [Inf β] (a₁ : α) (a₂ : α) (b₁ : β) (b₂ : β) : (a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂)

@[simp]

theorem Prod.fst_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) : (p ⊔ q).1 = p.1 ⊔ q.1

@[simp]

theorem Prod.fst_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) : (p ⊓ q).1 = p.1 ⊓ q.1

@[simp]

theorem Prod.snd_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) : (p ⊔ q).2 = p.2 ⊔ q.2

@[simp]

theorem Prod.snd_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) : (p ⊓ q).2 = p.2 ⊓ q.2

@[simp]

theorem Prod.swap_sup (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) : Prod.swap (p ⊔ q) = Prod.swap p ⊔ Prod.swap q

@[simp]

theorem Prod.swap_inf (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) : Prod.swap (p ⊓ q) = Prod.swap p ⊓ Prod.swap q

theorem Prod.sup_def (α : Type u) (β : Type v) [Sup α] [Sup β] (p : α × β) (q : α × β) : p ⊔ q = (p.1 ⊔ q.1, p.2 ⊔ q.2)

theorem Prod.inf_def (α : Type u) (β : Type v) [Inf α] [Inf β] (p : α × β) (q : α × β) : p ⊓ q = (p.1 ⊓ q.1, p.2 ⊓ q.2)

instance Prod.semilatticeSup (α : Type u) (β : Type v) [SemilatticeSup α] [SemilatticeSup β] : SemilatticeSup (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Prod.semilatticeInf (α : Type u) (β : Type v) [SemilatticeInf α] [SemilatticeInf β] : SemilatticeInf (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Prod.lattice (α : Type u) (β : Type v) [Lattice α] [Lattice β] : Lattice (α × β)

Equations

• One or more equations did not get rendered due to their size.

instance Prod.distribLattice (α : Type u) (β : Type v) [DistribLattice α] [DistribLattice β] : DistribLattice (α × β)

Equations

• One or more equations did not get rendered due to their size.

Subtypes of (semi-)lattices

@[reducible]

def Subtype.semilatticeSup {α : Type u} [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) : SemilatticeSup { x : α // P x }

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Subtype.semilatticeInf {α : Type u} [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) : SemilatticeInf { x : α // P x }

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

Equations

• One or more equations did not get rendered due to their size.

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subtype.coe_sup {α : Type u} [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) (x : Subtype P) (y : Subtype P) : ↑(x ⊔ y) = ↑x ⊔ ↑y

@[simp]

theorem Subtype.coe_inf {α : Type u} [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) (x : Subtype P) (y : Subtype P) : ↑(x ⊓ y) = ↑x ⊓ ↑y

@[simp]

theorem Subtype.mk_sup_mk {α : Type u} [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) {x : α} {y : α} (hx : P x) (hy : P y) : { val := x, property := hx } ⊔ { val := y, property := hy } = { val := x ⊔ y, property := (_ : P (x ⊔ y)) }

@[simp]

theorem Subtype.mk_inf_mk {α : Type u} [SemilatticeInf α] {P : α → Prop} (Pinf : ∀ ⦃x y : α⦄, P x → P y → P (x ⊓ y)) {x : α} {y : α} (hx : P x) (hy : P y) : { val := x, property := hx } ⊓ { val := y, property := hy } = { val := x ⊓ y, property := (_ : P (x ⊓ y)) }

@[reducible]

def Function.Injective.semilatticeSup {α : Type u} {β : Type v} [Sup α] [SemilatticeSup β] (f : α → β) (hf_inj : Function.Injective f) (map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) : SemilatticeSup α

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Function.Injective.semilatticeInf {α : Type u} {β : Type v} [Inf α] [SemilatticeInf β] (f : α → β) (hf_inj : Function.Injective f) (map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b) : SemilatticeInf α

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

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def Function.Injective.lattice {α : Type u} {β : Type v} [Sup α] [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

• One or more equations did not get rendered due to their size.

@[reducible]

def Function.Injective.distribLattice {α : Type u} {β : Type v} [Sup α] [Inf α] [DistribLattice β] (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) : DistribLattice α

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

Equations

• One or more equations did not get rendered due to their size.

instance ULift.instSemilatticeSupULift {α : Type u} [SemilatticeSup α] : SemilatticeSup (ULift.{v, u} α)

Equations

• ULift.instSemilatticeSupULift = Function.Injective.semilatticeSup ULift.down (_ : Function.Injective ULift.down) (_ : ∀ (a b : ULift.{v, u} α), (a ⊔ b).down = a.down ⊔ b.down)

instance ULift.instSemilatticeInfULift {α : Type u} [SemilatticeInf α] : SemilatticeInf (ULift.{v, u} α)

Equations

• ULift.instSemilatticeInfULift = Function.Injective.semilatticeInf ULift.down (_ : Function.Injective ULift.down) (_ : ∀ (a b : ULift.{v, u} α), (a ⊓ b).down = a.down ⊓ b.down)

instance ULift.instLatticeULift {α : Type u} [Lattice α] : Lattice (ULift.{v, u} α)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.instDistribLatticeULift {α : Type u} [DistribLattice α] : DistribLattice (ULift.{v, u} α)

Equations

• One or more equations did not get rendered due to their size.

instance ULift.instLinearOrderULift {α : Type u} [LinearOrder α] : LinearOrder (ULift.{v, u} α)

Equations

• One or more equations did not get rendered due to their size.

instance Bool.instDistribLattice : DistribLattice Bool

Equations

• Bool.instDistribLattice = inferInstance