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 #

source

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

Instances For

source

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

Instances For

source

@[simp]

theorem left_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} :

a < a ⊔ b ↔ ¬b ≤ a

source

@[simp]

theorem inf_lt_left {α : Type u} [SemilatticeInf α] {a b : α} :

a ⊓ b < a ↔ ¬a ≤ b

source

@[simp]

theorem right_lt_sup {α : Type u} [SemilatticeSup α] {a b : α} :

b < a ⊔ b ↔ ¬a ≤ b

source

@[simp]

theorem inf_lt_right {α : Type u} [SemilatticeInf α] {a b : α} :

a ⊓ b < b ↔ ¬b ≤ a

source

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

a < a ⊔ b ∨ b < a ⊔ b

source

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

a ⊓ b < a ∨ a ⊓ b < b

source

theorem le_iff_exists_sup {α : Type u} [SemilatticeSup α] {a b : α} :

a ≤ b ↔ ∃ (c : α), b = a ⊔ c

source

theorem le_iff_exists_inf {α : Type u} [SemilatticeInf α] {a b : α} :

b ≤ a ↔ ∃ (c : α), b = a ⊓ c

source

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

a ⊔ b = a ⊔ c

source

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

a ⊓ b = a ⊓ c

source

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

a ⊔ c = b ⊔ c

source

theorem inf_congr_right {α : Type u} [SemilatticeInf α] {a b c : α} (ha : b ⊓ c ≤ a) (hb : a ⊓ c ≤ b) :

a ⊓ c = b ⊓ c

source

theorem sup_eq_sup_iff_left {α : Type u} [SemilatticeSup α] {a b c : α} :

a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b

source

theorem inf_eq_inf_iff_left {α : Type u} [SemilatticeInf α] {a b c : α} :

a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c

source

theorem sup_eq_sup_iff_right {α : Type u} [SemilatticeSup α] {a b c : α} :

a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

source

theorem inf_eq_inf_iff_right {α : Type u} [SemilatticeInf α] {a b c : α} :

a ⊓ c = b ⊓ c ↔ b ⊓ c ≤ a ∧ a ⊓ c ≤ b

source

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

source

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

source

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

source

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

source

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

a < a ⊔ b ∨ b < a ⊔ b

source

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

a ⊓ b < a ∨ a ⊓ b < b

source

theorem ite_le_sup {α : Type u} [SemilatticeSup α] (a b : α) (P : Prop) [Decidable P] :

(if P then a else b) ≤ a ⊔ b

source

theorem inf_le_ite {α : Type u} [SemilatticeInf α] (a b : α) (P : Prop) [Decidable P] :

a ⊓ b ≤ if P then a else b

source

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

x ⊔ y = x ⊔ y

source

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

x ⊓ y = x ⊓ y

source

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

A = B

source

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

A = B

source

@[instance_reducible]

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

SemilatticeSup αᵒᵈ

source

@[instance_reducible]

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

SemilatticeInf αᵒᵈ

source

theorem SemilatticeSup.dual_dual (α : Type u_1) [H : SemilatticeSup α] :

OrderDual.instSemilatticeSup αᵒᵈ = H

source

theorem SemilatticeInf.dual_dual (α : Type u_1) [H : SemilatticeInf α] :

OrderDual.instSemilatticeInf αᵒᵈ = H

Lattices #

source

@[instance_reducible]

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

Lattice αᵒᵈ

source

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

source

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

Instances For

source

@[simp]

theorem inf_eq_sup {α : Type u} [Lattice α] {a b : α} :

a ⊓ b = a ⊔ b ↔ a = b

source

@[simp]

theorem sup_eq_inf {α : Type u} [Lattice α] {a b : α} :

a ⊔ b = a ⊓ b ↔ a = b

source

@[simp]

theorem inf_lt_sup {α : Type u} [Lattice α] {a b : α} :

a ⊓ b < a ⊔ b ↔ a ≠ b

source

theorem inf_eq_and_sup_eq_iff {α : Type u} [Lattice α] {a b c : α} :

a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

source

theorem sup_eq_and_inf_eq_iff {α : Type u} [Lattice α] {a b c : α} :

a ⊔ b = c ∧ a ⊓ b = c ↔ a = c ∧ b = c

source

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

A = B

source

@[instance_reducible]

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

DistribLattice αᵒᵈ

Lattices derived from linear orders #

source

@[instance_reducible, instance 100]

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

Lattice α

source

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

p (max a b)

source

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

p (min a b)

source

theorem le_sup_iff {α : Type u} [LinearOrder α] {a b c : α} :

a ≤ max b c ↔ a ≤ b ∨ a ≤ c

source

theorem inf_le_iff {α : Type u} [LinearOrder α] {a b c : α} :

min b c ≤ a ↔ b ≤ a ∨ c ≤ a

source

theorem lt_sup_iff {α : Type u} [LinearOrder α] {a b c : α} :

a < max b c ↔ a < b ∨ a < c

source

theorem inf_lt_iff {α : Type u} [LinearOrder α] {a b c : α} :

min b c < a ↔ b < a ∨ c < a

source

theorem sup_lt_iff {α : Type u} [LinearOrder α] {a b c : α} :

max b c < a ↔ b < a ∧ c < a

source

theorem lt_inf_iff {α : Type u} [LinearOrder α] {a b c : α} :

a < min b c ↔ a < b ∧ a < c

source

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)

source

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)

source

theorem sup_eq_maxDefault {α : Type u} [SemilatticeSup α] [DecidableLE α] [Std.Total fun (x1 x2 : α) => x1 ≤ x2] :

(fun (x1 x2 : α) => x1 ⊔ x2) = maxDefault

source

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

(fun (x1 x2 : α) => x1 ⊓ x2) = minDefault

source

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

Instances For

source

@[instance_reducible, instance 100]

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

DistribLattice α

source

@[instance_reducible]

instance instDistribLatticeNat :

DistribLattice ℕ

source

@[instance_reducible]

instance instLatticeInt :

Lattice ℤ

Dual order #

source

@[simp]

theorem ofDual_sup {α : Type u} [Min α] (a b : αᵒᵈ) :

OrderDual.ofDual (a ⊔ b) = OrderDual.ofDual a ⊓ OrderDual.ofDual b

source

@[simp]

theorem ofDual_inf {α : Type u} [Max α] (a b : αᵒᵈ) :

OrderDual.ofDual (a ⊓ b) = OrderDual.ofDual a ⊔ OrderDual.ofDual b

source

@[simp]

theorem toDual_sup {α : Type u} [Max α] (a b : α) :

OrderDual.toDual (a ⊔ b) = OrderDual.toDual a ⊓ OrderDual.toDual b

source

@[simp]

theorem toDual_inf {α : Type u} [Min α] (a b : α) :

OrderDual.toDual (a ⊓ b) = OrderDual.toDual a ⊔ OrderDual.toDual b

source

theorem ofDual_max {α : Type u} [LinearOrder α] (a b : αᵒᵈ) :

OrderDual.ofDual (max a b) = min (OrderDual.ofDual a) (OrderDual.ofDual b)

source

theorem ofDual_min {α : Type u} [LinearOrder α] (a b : αᵒᵈ) :

OrderDual.ofDual (min a b) = max (OrderDual.ofDual a) (OrderDual.ofDual b)

source

theorem toDual_max {α : Type u} [LinearOrder α] (a b : α) :

OrderDual.toDual (max a b) = min (OrderDual.toDual a) (OrderDual.toDual b)

source

theorem toDual_min {α : Type u} [LinearOrder α] (a b : α) :

OrderDual.toDual (min a b) = max (OrderDual.toDual a) (OrderDual.toDual b)

Function lattices #

source

@[instance_reducible]

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

Max ((i : ι) → α' i)

source

@[instance_reducible]

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

Min ((i : ι) → α' i)

source

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

source

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

source

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

source

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

source

@[instance_reducible]

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

SemilatticeSup ((i : ι) → α' i)

source

@[instance_reducible]

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

SemilatticeInf ((i : ι) → α' i)

source

@[instance_reducible]

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

Lattice ((i : ι) → α' i)

source

@[instance_reducible]

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

DistribLattice ((i : ι) → α' i)

source

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

source

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 #

source

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.

source

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.

source

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.

source

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.

source

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

f x ⊔ f y ≤ f (x ⊔ y)

source

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

f (x ⊓ y) ≤ f x ⊓ f y

source

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

Monotone f

source

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

Monotone f

source

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

source

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

source

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

Monotone f

source

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

Monotone f

source

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

f (max x y) = f x ⊔ f y

source

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

f (min x y) = f x ⊓ f y

source

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

(∃ (x : α), x₀ ≤ x ∧ P x) ↔ ∃ (x : α), P x

source

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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

source

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.

source

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.

source

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.

source

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.

source

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

f (x ⊔ y) ≤ f x ⊓ f y

source

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

f x ⊔ f y ≤ f (x ⊓ y)

source

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

f (max x y) = f x ⊓ f y

source

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

f (min x y) = f x ⊔ f y

source

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

(∃ (x : α), x ≤ x₀ ∧ P x) ↔ ∃ (x : α), P x

source

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

source

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.

source

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.

source

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.

source

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.

source

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

source

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

source

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

source

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 #

source

@[instance_reducible]

instance Prod.instMax_mathlib (α : Type u) (β : Type v) [Max α] [Max β] :

Max (α × β)

source

@[instance_reducible]

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

Min (α × β)

source

@[simp]

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

(a₁, b₁) ⊔ (a₂, b₂) = (a₁ ⊔ a₂, b₁ ⊔ b₂)

source

@[simp]

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

(a₁, b₁) ⊓ (a₂, b₂) = (a₁ ⊓ a₂, b₁ ⊓ b₂)

source

@[simp]

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

(p ⊔ q).fst = p.fst ⊔ q.fst

source

@[simp]

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

(p ⊓ q).fst = p.fst ⊓ q.fst

source

@[simp]

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

(p ⊔ q).snd = p.snd ⊔ q.snd

source

@[simp]

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

(p ⊓ q).snd = p.snd ⊓ q.snd

source

@[simp]

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

(p ⊔ q).swap = p.swap ⊔ q.swap

source

@[simp]

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

(p ⊓ q).swap = p.swap ⊓ q.swap

source

theorem Prod.sup_def (α : Type u) (β : Type v) [Max α] [Max β] (p q : α × β) :

p ⊔ q = (p.fst ⊔ q.fst, p.snd ⊔ q.snd)

source

theorem Prod.inf_def (α : Type u) (β : Type v) [Min α] [Min β] (p q : α × β) :

p ⊓ q = (p.fst ⊓ q.fst, p.snd ⊓ q.snd)

source

@[instance_reducible]

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

SemilatticeSup (α × β)

source

@[instance_reducible]

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

SemilatticeInf (α × β)

source

@[instance_reducible]

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

Lattice (α × β)

source

@[instance_reducible]

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

DistribLattice (α × β)

Subtypes of (semi-)lattices #

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

source

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

source

@[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, ⋯⟩

source

@[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, ⋯⟩

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

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

Instances For

source

@[reducible, inline]