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

Notation

• 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 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_ge (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 ≤ sup a b

  The supremum is an upper bound on the first argument

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

  The supremum is an upper bound on the second argument

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

  The supremum is the least upper bound

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_ge (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 : α) : inf a b ≤ a

  The infimum is a lower bound on the first argument

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

  The infimum is a lower bound on the second argument

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

  The infimum is the greatest lower bound

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

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

@[instance_reducible]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

theorem inf_lt_of_right_lt {α : Type u} [SemilatticeInf α] {a b c : α} (h : 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 le_inf_iff {α : Type u} [SemilatticeInf α] {c a b : α} : c ≤ a ⊓ b ↔ c ≤ a ∧ c ≤ b

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of the forward direction of sup_eq_left.

@[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 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_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 = b → b ≤ a

Alias of the forward direction of inf_eq_right.

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 left_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} : a < a ⊔ b ↔ ¬b ≤ a

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

theorem le_iff_exists_inf {α : Type u} [SemilatticeInf α] {a b : α} : b ≤ a ↔ ∃ (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 inf_le_inf {α : Type u} [SemilatticeInf α] {a b c d : α} (h₁ : b ≤ a) (h₂ : d ≤ c) : b ⊓ d ≤ a ⊓ c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

instance instAssociativeMin_mathlib {α : Type u} [SemilatticeInf α] : 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 inf_left_right_swap {α : Type u} [SemilatticeInf α] (a b c : α) : a ⊓ b ⊓ c = c ⊓ b ⊓ a

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

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

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

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

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

theorem inf_left_comm {α : Type u} [SemilatticeInf α] (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 inf_right_comm {α : Type u} [SemilatticeInf α] (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 inf_inf_inf_comm {α : Type u} [SemilatticeInf α] (a b c d : α) : a ⊓ b ⊓ (c ⊓ d) = a ⊓ c ⊓ (b ⊓ d)

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

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

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

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

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

theorem inf_inf_distrib_left {α : Type u} [SemilatticeInf α] (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 inf_inf_distrib_right {α : Type u} [SemilatticeInf α] (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 inf_congr_left {α : Type u} [SemilatticeInf α] {a b c : α} (hb : a ⊓ c ≤ b) (hc : a ⊓ b ≤ c) : 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 inf_congr_right {α : Type u} [SemilatticeInf α] {a b c : α} (ha : b ⊓ c ≤ a) (hb : a ⊓ c ≤ b) : 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 inf_eq_inf_iff_left {α : Type u} [SemilatticeInf α] {a b c : α} : a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c

theorem sup_eq_sup_iff_right {α : Type u} [SemilatticeSup α] {a b c : α} : a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ 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.lt_sup_or_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} (hab : a ≠ b) : a < a ⊔ b ∨ b < a ⊔ b

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

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

theorem inf_le_ite {α : Type u} [SemilatticeInf α] (a b : α) (P : Prop) [Decidable P] : a ⊓ b ≤ if P then a else 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 SemilatticeInf.ext_inf {α : Type u_1} {A B : SemilatticeInf α} (H : ∀ (y x : α), y ≤ x ↔ y ≤ x) (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 SemilatticeInf.ext {α : Type u_1} {A B : SemilatticeInf α} (H : ∀ (y x : α), y ≤ x ↔ y ≤ x) : A = B

@[instance_reducible]

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

Equations

• OrderDual.instSemilatticeSup α = { toPartialOrder := OrderDual.instPartialOrder α, sup := fun (a b : αᵒᵈ) => SemilatticeInf.inf a b, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[instance_reducible]

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

Equations

• OrderDual.instSemilatticeInf α = { toPartialOrder := OrderDual.instPartialOrder α, inf := fun (a b : αᵒᵈ) => SemilatticeSup.sup a b, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

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

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

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_ge (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 ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → 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_reducible]

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

Equations

• OrderDual.instLattice α = { toSemilatticeSup := OrderDual.instSemilatticeSup α, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_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.mk' sup_comm sup_assoc sup_idem).toPartialOrder = (SemilatticeInf.mk' inf_comm inf_assoc inf_idem).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).

@[instance_reducible]

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

• 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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem inf_eq_and_sup_eq_iff {α : Type u} [Lattice α] {a b c : α} : a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

theorem sup_eq_and_inf_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 inf_eq_iff_sup_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_ge (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 ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → 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

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

@[instance_reducible]

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

Equations

• OrderDual.instDistribLattice α = { toLattice := OrderDual.instLattice α, le_sup_inf := ⋯ }

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 = { toLattice := inst✝, le_sup_inf := ⋯ }

Lattices derived from linear orders

@[instance_reducible, instance 100]

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

Equations

• LinearOrder.toLattice = { toPartialOrder := inst✝.toPartialOrder, sup := max, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯, inf := min, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem lt_inf_iff {α : Type u} [LinearOrder α] {a b c : α} : a < min 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 α] [DecidableLE α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : (fun (x1 x2 : α) => x1 ⊔ x2) = maxDefault

theorem inf_eq_minDefault {α : Type u} [SemilatticeInf α] [DecidableLE α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : (fun (x1 x2 : α) => x1 ⊓ x2) = minDefault

@[reducible, inline]

abbrev Lattice.toLinearOrder (α : Type u) [Lattice α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] : LinearOrder α

A lattice with total order is a linear order.

See note [reducible non-instances].

Equations

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

@[instance_reducible, instance 100]

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

Equations

• instDistribLatticeOfLinearOrder = { toLattice := LinearOrder.toLattice, le_sup_inf := ⋯ }

@[instance_reducible]

instance instDistribLatticeNat : DistribLattice ℕ

Equations

• instDistribLatticeNat = inferInstance

@[instance_reducible]

instance instLatticeInt : Lattice ℤ

Equations

• instLatticeInt = inferInstance

Dual order

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Function lattices

@[instance_reducible]

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 }

@[instance_reducible]

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.sup_apply {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Max (α' i)] (f g : (i : ι) → α' i) (i : ι) : (f ⊔ g) 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.sup_def {ι : Type u_1} {α' : ι → Type u_2} [(i : ι) → Max (α' i)] (f g : (i : ι) → α' i) : f ⊔ g = fun (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_reducible]

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

Equations

• Pi.instSemilatticeSup = { toPartialOrder := Pi.partialOrder, sup := fun (x y : (i : ι) → α' i) (i : ι) => x i ⊔ y i, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[instance_reducible]

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

Equations

• Pi.instSemilatticeInf = { toPartialOrder := Pi.partialOrder, inf := fun (x y : (i : ι) → α' i) (i : ι) => x i ⊓ y i, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

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

Equations

• Pi.instLattice = { toSemilatticeSup := Pi.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

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

Equations

• Pi.instDistribLattice = { toLattice := Pi.instLattice, le_sup_inf := ⋯ }

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

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_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_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_sup {α : Type u} {β : Type v} [SemilatticeSup α] [SemilatticeSup β] {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.map_sup {α : Type u} {β : Type v} [LinearOrder α] [SemilatticeSup β] {f : α → β} (hf : Monotone f) (x y : α) : f (max x y) = f x ⊔ f y

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

theorem exists_ge_and_iff_exists {α : Type u} [SemilatticeSup α] {P : α → Prop} {x₀ : α} (hP : Monotone P) : (∃ (x : α), x₀ ≤ x ∧ P x) ↔ ∃ (x : α), P x

theorem exists_and_iff_of_monotone {α : Type u} [SemilatticeSup α] {P Q : α → Prop} (hP : Monotone P) (hQ : Monotone Q) : ((∃ (x : α), P x) ∧ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ∧ Q x

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_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.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.map_sup {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [LinearOrder α] [SemilatticeSup β] (hf : MonotoneOn f s) (hx : x ∈ s) (hy : y ∈ s) : f (max 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 (min 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 antitone functions is an antitone 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 antitone functions is an antitone 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 antitone functions is an antitone 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 antitone functions is an antitone 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 (max x y) = f x ⊓ f y

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

theorem exists_le_and_iff_exists {α : Type u} [SemilatticeInf α] {P : α → Prop} {x₀ : α} (hP : Antitone P) : (∃ (x : α), x ≤ x₀ ∧ P x) ↔ ∃ (x : α), P x

theorem exists_and_iff_of_antitone {α : Type u} [SemilatticeInf α] {P Q : α → Prop} (hP : Antitone P) (hQ : Antitone Q) : ((∃ (x : α), P x) ∧ ∃ (x : α), Q x) ↔ ∃ (x : α), P x ∧ Q x

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 (max 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 (min x y) = f x ⊔ f y

Products of (semi-)lattices

@[instance_reducible]

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_reducible]

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_reducible]

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

Equations

• Prod.instSemilatticeSup α β = { toPartialOrder := Prod.instPartialOrder α β, sup := fun (a b : α × β) => (a.fst ⊔ b.fst, a.snd ⊔ b.snd), le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instSemilatticeInf α β = { toPartialOrder := Prod.instPartialOrder α β, inf := fun (a b : α × β) => (a.fst ⊓ b.fst, a.snd ⊓ b.snd), inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instLattice α β = { toSemilatticeSup := Prod.instSemilatticeSup α β, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

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

Equations

• Prod.instDistribLattice α β = { toLattice := Prod.instLattice α β, le_sup_inf := ⋯ }

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

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

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

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

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

• 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 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 α] [LE α] [LT α] [SemilatticeSup β] (f : α → β) (hf_inj : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (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, inline]

abbrev Function.Injective.semilatticeInf {α : Type u} {β : Type v} [Min α] [LE α] [LT α] [SemilatticeInf β] (f : α → β) (hf_inj : Injective f) (le : ∀ {x y : α}, f y ≤ f x ↔ y ≤ x) (lt : ∀ {x y : α}, f y < f x ↔ y < x) (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, inline]

abbrev Function.Injective.lattice {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [Lattice β] (f : α → β) (hf_inj : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (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, inline]

abbrev Function.Injective.distribLattice {α : Type u} {β : Type v} [Max α] [Min α] [LE α] [LT α] [DistribLattice β] (f : α → β) (hf_inj : Injective f) (le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y : α}, f x < f y ↔ x < y) (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 le lt map_sup map_inf = { toLattice := Function.Injective.lattice f hf_inj ⋯ ⋯ map_sup map_inf, le_sup_inf := ⋯ }

@[reducible, inline]

abbrev Subtype.distribLattice {α : Type u} [DistribLattice α] {P : α → Prop} (Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)) (Pinf : ∀ ⦃s t : α⦄, P s → P t → P (s ⊓ t)) : DistribLattice (Subtype P)

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

Equations

• Subtype.distribLattice Psup Pinf = Function.Injective.distribLattice (fun (a : Subtype P) => ↑a) ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.preorder {α : Type u} {β : Type v} (e : α ≃ β) [Preorder β] : Preorder α

Transfer Preorder across an Equiv.

Equations

• e.preorder = Function.Injective.preorder ⇑e ⋯ ⋯

@[reducible, inline]

abbrev Equiv.partialOrder {α : Type u} {β : Type v} (e : α ≃ β) [PartialOrder β] : PartialOrder α

Transfer PartialOrder across an Equiv.

Equations

• e.partialOrder = Function.Injective.partialOrder ⇑e ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.linearOrder {α : Type u} {β : Type v} (e : α ≃ β) [LinearOrder β] [DecidableEq α] : LinearOrder α

Transfer LinearOrder across an Equiv.

Equations

• e.linearOrder = Function.Injective.linearOrder ⇑e ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.semilatticeSup {α : Type u} {β : Type v} (e : α ≃ β) [SemilatticeSup β] : SemilatticeSup α

Transfer SemilatticeSup across an Equiv.

Equations

• e.semilatticeSup = Function.Injective.semilatticeSup ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.semilatticeInf {α : Type u} {β : Type v} (e : α ≃ β) [SemilatticeInf β] : SemilatticeInf α

Transfer SemilatticeInf across an Equiv.

Equations

• e.semilatticeInf = Function.Injective.semilatticeInf ⇑e ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.lattice {α : Type u} {β : Type v} (e : α ≃ β) [Lattice β] : Lattice α

Transfer Lattice across an Equiv.

Equations

• e.lattice = Function.Injective.lattice ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

@[reducible, inline]

abbrev Equiv.distribLattice {α : Type u} {β : Type v} (e : α ≃ β) [DistribLattice β] : DistribLattice α

Transfer DistribLattice across an Equiv.

Equations

• e.distribLattice = Function.Injective.distribLattice ⇑e ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• ULift.instLattice = { toSemilatticeSup := ULift.instSemilatticeSup, inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• ULift.instLinearOrder = Function.Injective.linearOrder ULift.down ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance Bool.instPartialOrder : PartialOrder Bool

Equations

• Bool.instPartialOrder = inferInstance

@[instance_reducible]

instance Bool.instDistribLattice : DistribLattice Bool

Equations

• Bool.instDistribLattice = inferInstance

theorem pairwise_iff_lt {α : Type u} [LinearOrder α] {p : α → α → Prop} [Std.Symm p] : Pairwise p ↔ ∀ ⦃a b : α⦄, a < b → p a b

theorem pairwise_iff_gt {α : Type u} [LinearOrder α] {p : α → α → Prop} [Std.Symm p] : Pairwise p ↔ ∀ ⦃a b : α⦄, b < a → p a b

theorem Pairwise.of_lt {α : Type u} [LinearOrder α] {p : α → α → Prop} [Std.Symm p] : (∀ ⦃a b : α⦄, a < b → p a b) → Pairwise p

Alias of the reverse direction of pairwise_iff_lt.

theorem Pairwise.of_gt {α : Type u} [LinearOrder α] {p : α → α → Prop} [Std.Symm p] : (∀ ⦃a b : α⦄, b < a → p a b) → Pairwise p

Alias of the reverse direction of pairwise_iff_gt.