Basic properties of lattices

This file contains some basic results, alternative constructors and instances for (semi)lattices. For the definitions, see Mathlib.Order.Defs.Lattice.

Main declarations

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

TODO

• Alternative constructors for distributive lattices from the other distributive properties

Tags

semilattice, lattice

Semilattices

@[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 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_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 sup_eq_sup_mono_left {α : Type u} [SemilatticeSup α] {a b c d : α} (h : a ⊔ b = a ⊔ c) (had : a ≤ d) : d ⊔ b = d ⊔ c

theorem inf_eq_inf_mono_left {α : Type u} [SemilatticeInf α] {a b c d : α} (h : a ⊓ b = a ⊓ c) (had : d ≤ a) : d ⊓ b = d ⊓ c

theorem sup_eq_sup_mono_right {α : Type u} [SemilatticeSup α] {a b c d : α} (h : a ⊔ c = b ⊔ c) (hcd : c ≤ d) : a ⊔ d = b ⊔ d

theorem inf_eq_inf_mono_right {α : Type u} [SemilatticeInf α] {a b c d : α} (h : a ⊓ c = b ⊓ c) (hcd : d ≤ c) : a ⊓ d = b ⊓ d

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

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

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

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

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

@[instance_reducible]

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

Equations

• OrderDual.instDistribLattice α = { toLattice := OrderDual.instLattice α, 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)

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

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

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

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

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

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.{v, u} α)

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

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.{v, u} α)

Equations

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

@[instance_reducible]

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

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.