(Semi-)lattices

Semilattices are partially ordered sets with join (least upper bound, or sup) or meet (greatest lower 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

def exactSubsetOfSSubset : Mathlib.Tactic.GCongr.ForwardExt

See if the term is a ⊂ b and the goal is a ⊆ b.

Equations

• exactSubsetOfSSubset = { eval := fun (h : Lean.Expr) (goal : Lean.MVarId) => do let __do_lift ← Lean.Meta.mkAppM `subset_of_ssubset #[h] goal.assignIfDefeq __do_lift }

Join-semilattices

class SemilatticeSup (α : Type u) extends 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.

• 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
• sup : α → α → α

  The binary supremum, used to derive Max α

• le_sup_left (a b : α) : a ≤ SemilatticeSup.sup a b

  The supremum is an upper bound on the first argument

• le_sup_right (a b : α) : b ≤ SemilatticeSup.sup a b

  The supremum is an upper bound on the second argument

• sup_le (a b c : α) : a ≤ c → b ≤ c → SemilatticeSup.sup a b ≤ c

  The supremum is the least upper bound

instance SemilatticeSup.toMax {α : Type u} [SemilatticeSup α] : Max α

Equations

• SemilatticeSup.toMax = { max := fun (a b : α) => SemilatticeSup.sup a b }

def SemilatticeSup.mk' {α : Type u_1} [Max α] (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

• SemilatticeSup.mk' sup_comm sup_assoc sup_idem = SemilatticeSup.mk (fun (x1 x2 : α) => x1 ⊔ x2) ⋯ ⋯ ⋯

@[simp]

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

@[deprecated le_sup_left]

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

Alias of le_sup_left.

@[simp]

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

@[deprecated le_sup_right]

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

Alias of le_sup_right.

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.

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

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 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 instIdempotentOpMax_mathlib {α : Type u} [SemilatticeSup α] : Std.IdempotentOp fun (x1 x2 : α) => x1 ⊔ x2

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

instance instCommutativeMax_mathlib {α : Type u} [SemilatticeSup α] : Std.Commutative fun (x1 x2 : α) => x1 ⊔ x2

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

instance instAssociativeMax_mathlib {α : Type u} [SemilatticeSup α] : Std.Associative fun (x1 x2 : α) => x1 ⊔ x2

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

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

• 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 : α → α → α

  The binary infimum, used to derive Min α

• inf_le_left (a b : α) : SemilatticeInf.inf a b ≤ a

  The infimum is a lower bound on the first argument

• inf_le_right (a b : α) : SemilatticeInf.inf a b ≤ b

  The infimum is a lower bound on the second argument

• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c

  The infimum is the greatest lower bound

instance SemilatticeInf.toMin {α : Type u} [SemilatticeInf α] : Min α

Equations

• SemilatticeInf.toMin = { min := fun (a b : α) => SemilatticeInf.inf a b }

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

Equations

• OrderDual.instSemilatticeSup α = SemilatticeSup.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

Equations

• OrderDual.instSemilatticeInf α = SemilatticeInf.mk max ⋯ ⋯ ⋯

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

@[simp]

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

@[deprecated inf_le_left]

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

Alias of inf_le_left.

@[simp]

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

@[deprecated inf_le_right]

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

Alias of inf_le_right.

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 instIdempotentOpMin_mathlib {α : Type u} [SemilatticeInf α] : Std.IdempotentOp fun (x1 x2 : α) => x1 ⊓ x2

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

instance instCommutativeMin_mathlib {α : Type u} [SemilatticeInf α] : Std.Commutative fun (x1 x2 : α) => x1 ⊓ x2

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

instance instAssociativeMin_mathlib {α : Type u} [SemilatticeInf α] : Std.Associative fun (x1 x2 : α) => x1 ⊓ x2

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

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

theorem SemilatticeInf.dual_dual (α : Type u_1) [H : SemilatticeInf α] : OrderDual.instSemilatticeInf αᵒᵈ = 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} [Min α] (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.instSemilatticeInf αᵒᵈ

Lattices

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

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

• 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
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ SemilatticeSup.sup a b
• le_sup_right (a b : α) : b ≤ SemilatticeSup.sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → SemilatticeSup.sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c

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

Equations

• OrderDual.instLattice α = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

theorem semilatticeSup_mk'_partialOrder_eq_semilatticeInf_mk'_partialOrder {α : Type u_1} [Max α] [Min α] (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} [Max α] [Min α] (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 = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

• 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
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ SemilatticeSup.sup a b
• le_sup_right (a b : α) : b ≤ SemilatticeSup.sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → SemilatticeSup.sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf 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 α] (a b c : α) : a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)

theorem sup_inf_right {α : Type u} [DistribLattice α] (a b c : α) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

theorem inf_sup_left {α : Type u} [DistribLattice α] (a b c : α) : a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c

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

Equations

• OrderDual.instDistribLattice α = DistribLattice.mk ⋯

theorem inf_sup_right {α : Type u} [DistribLattice α] (a b c : α) : (a ⊔ b) ⊓ c = a ⊓ c ⊔ b ⊓ c

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, inline]

abbrev 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 ⋯

Lattices derived from linear orders

@[instance 100]

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

Equations

• LinearOrder.toLattice = Lattice.mk min ⋯ ⋯ ⋯

@[deprecated]

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

@[deprecated]

theorem inf_eq_min {α : Type u} [LinearOrder α] {a b : α} : a ⊓ b = 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 : α) : a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

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

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

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

@[reducible, inline]

abbrev Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] [DecidableRel fun (x1 x2 : α) => x1 < x2] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] : LinearOrder α

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations

• Lattice.toLinearOrder α = LinearOrder.mk ⋯ inst✝² inst✝³ inst✝¹ ⋯ ⋯ ⋯

@[instance 100]

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

Equations

• instDistribLatticeOfLinearOrder = DistribLattice.mk ⋯

instance instDistribLatticeNat : DistribLattice ℕ

Equations

• instDistribLatticeNat = inferInstance

instance instLatticeInt : Lattice ℤ

Equations

• instLatticeInt = inferInstance

Dual order

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Function lattices

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

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

Equations

• Pi.instSemilatticeSup = SemilatticeSup.mk (fun (x x_1 : (i : ι) → α' i) (x_2 : ι) => x x_2 ⊔ x_1 x_2) ⋯ ⋯ ⋯

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

Equations

• Pi.instSemilatticeInf = SemilatticeInf.mk (fun (x x_1 : (i : ι) → α' i) (x_2 : ι) => x x_2 ⊓ x_1 x_2) ⋯ ⋯ ⋯

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

Equations

• Pi.instLattice = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

Equations

• Pi.instDistribLattice = DistribLattice.mk ⋯

theorem Function.update_sup {ι : Type u_1} {π : ι → Type u_2} [DecidableEq ι] [(i : ι) → SemilatticeSup (π i)] (f : (i : ι) → π i) (i : ι) (a 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 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 : α) => 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 : α) => 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_le_left {α : Type u} {β : Type v} [SemilatticeInf α] [Preorder β] {f : α → β} (h : ∀ (x y : α), f (x ⊓ y) ≤ f x) : Monotone f

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

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_left_le_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [Preorder β] {f : α → β} (h : ∀ (x y : α), f x ≤ f (x ⊔ y)) : Monotone f

theorem Monotone.of_le_map_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} (h : ∀ (x y : α), f x ⊔ f y ≤ f (x ⊔ 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 : α) => 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 : α) => 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 : α) => 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 : α) => 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 : α) => 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 : α) => 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.instMax_mathlib (α : Type u) (β : Type v) [Max α] [Max β] : Max (α × β)

Equations

• Prod.instMax_mathlib α β = { max := fun (p q : α × β) => (p.fst ⊔ q.fst, p.snd ⊔ q.snd) }

instance Prod.instMin_mathlib (α : Type u) (β : Type v) [Min α] [Min β] : Min (α × β)

Equations

• Prod.instMin_mathlib α β = { min := fun (p q : α × β) => (p.fst ⊓ q.fst, p.snd ⊓ q.snd) }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Prod.sup_def (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) : p ⊔ q = (p.fst ⊔ q.fst, p.snd ⊔ q.snd)

theorem Prod.inf_def (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) : p ⊓ q = (p.fst ⊓ q.fst, p.snd ⊓ q.snd)

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

Equations

• Prod.instSemilatticeSup α β = SemilatticeSup.mk (fun (a b : α × β) => (a.fst ⊔ b.fst, a.snd ⊔ b.snd)) ⋯ ⋯ ⋯

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

Equations

• Prod.instSemilatticeInf α β = SemilatticeInf.mk (fun (a b : α × β) => (a.fst ⊓ b.fst, a.snd ⊓ b.snd)) ⋯ ⋯ ⋯

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

Equations

• Prod.instLattice α β = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

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

Equations

• Prod.instDistribLattice α β = DistribLattice.mk ⋯

Subtypes of (semi-)lattices

@[reducible, inline]

abbrev 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

• Subtype.semilatticeSup Psup = SemilatticeSup.mk (fun (x y : { x : α // P x }) => ⟨↑x ⊔ ↑y, ⋯⟩) ⋯ ⋯ ⋯

@[reducible, inline]

abbrev 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

• Subtype.semilatticeInf Pinf = SemilatticeInf.mk (fun (x y : { x : α // P x }) => ⟨↑x ⊓ ↑y, ⋯⟩) ⋯ ⋯ ⋯

@[reducible, inline]

abbrev 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 = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

@[simp]

theorem Subtype.coe_sup {α : Type u} [SemilatticeSup α] {P : α → Prop} (Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)) (x 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 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) : ⟨x, hx⟩ ⊔ ⟨y, hy⟩ = ⟨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) : ⟨x, hx⟩ ⊓ ⟨y, hy⟩ = ⟨x ⊓ y, ⋯⟩

@[reducible, inline]

abbrev Function.Injective.semilatticeSup {α : Type u} {β : Type v} [Max α] [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

• Function.Injective.semilatticeSup f hf_inj map_sup = SemilatticeSup.mk (fun (a b : α) => a ⊔ b) ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.semilatticeInf {α : Type u} {β : Type v} [Min α] [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

• Function.Injective.semilatticeInf f hf_inj map_inf = SemilatticeInf.mk (fun (a b : α) => a ⊓ b) ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.lattice {α : Type u} {β : Type v} [Max α] [Min α] [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 = Lattice.mk SemilatticeInf.inf ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Function.Injective.distribLattice {α : Type u} {β : Type v} [Max α] [Min α] [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

• Function.Injective.distribLattice f hf_inj map_sup map_inf = DistribLattice.mk ⋯

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

Equations

• ULift.instSemilatticeSup = Function.Injective.semilatticeSup ULift.down ⋯ ⋯

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

Equations

• ULift.instSemilatticeInf = Function.Injective.semilatticeInf ULift.down ⋯ ⋯

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

Equations

• ULift.instLattice = Function.Injective.lattice ULift.down ⋯ ⋯ ⋯

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

Equations

• ULift.instDistribLattice = Function.Injective.distribLattice ULift.down ⋯ ⋯ ⋯

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

Equations

• ULift.instLinearOrder = LinearOrder.liftWithOrd ULift.down ⋯ ⋯ ⋯ ⋯

instance Bool.instDistribLattice : DistribLattice Bool

Equations

• Bool.instDistribLattice = inferInstance