(Semi-)lattices #
Semilattices are partially ordered sets with join (greatest lower bound, or sup
) or
meet (least upper bound, or inf
) operations. Lattices are posets that are both
join-semilattices and meet-semilattices.
Distributive lattices are lattices which satisfy any of four equivalent distributivity properties,
of sup
over inf
, on the left or on the right.
Main declarations #
-
SemilatticeSup
: a type class for join semilattices -
SemilatticeSup.mk'
: an alternative constructor forSemilatticeSup
via proofs that⊔⊔
is commutative, associative and idempotent. -
SemilatticeInf
: a type class for meet semilattices -
SemilatticeSup.mk'
: an alternative constructor forSemilatticeInf
via proofs that⊓⊓
is commutative, associative and idempotent. -
Lattice
: a type class for lattices -
Lattice.mk'
: an alternative constructor forLattice
via profs that⊔⊔
and⊓⊓
are commutative, associative and satisfy a pair of "absorption laws". -
DistribLattice
: a type class for distributive lattices.
Notations #
a ⊔ b⊔ b
: the supremum or join ofa
andb
a ⊓ b⊓ b
: the infimum or meet ofa
andb
TODO #
- (Semi-)lattice homomorphisms
- Alternative constructors for distributive lattices from the other distributive properties
Tags #
semilattice, lattice
Join-semilattices #
The supremum is an upper bound on the first argument
The supremum is an upper bound on the second argument
The supremum is the least upper bound
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.
Instances
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≤ b
unfolds to a ⊔ b = b⊔ b = b
; cf. sup_eq_right
.
Equations
- One or more equations did not get rendered due to their size.
Equations
- instSupOrderDual α = { sup := fun x x_1 => x ⊓ x_1 }
Equations
- instInfOrderDual α = { inf := fun x x_1 => x ⊔ x_1 }
Alias of the reverse direction of sup_eq_left
.
Alias of the forward direction of sup_eq_right
.
Alias of the reverse direction of sup_eq_right
.
If f
is monotone, g
is antitone, and f ≤ g≤ g
, then for all a
, b
we have f a ≤ g b≤ g b
.
Meet-semilattices #
The infimum is a lower bound on the first argument
The infimum is a lower bound on the second argument
The infimum is the greatest lower bound
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.
Instances
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Alias of the forward direction of inf_eq_left
.
Alias of the reverse direction of inf_eq_left
.
Alias of the reverse direction of inf_eq_right
.
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≤ b
unfolds to b ⊓ a = a⊓ a = a
; cf. inf_eq_right
.
Equations
- SemilatticeInf.mk' inf_comm inf_assoc inf_idem = OrderDual.semilatticeInf αᵒᵈ
Lattices #
The infimum is a lower bound on the first argument
The infimum is a lower bound on the second argument
The infimum is the greatest lower bound
A lattice is a join-semilattice which is also a meet-semilattice.
Instances
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⊔ a ⊓ b = a⊓ b = a
)
and inf_sup_self
(a ⊓ (a ⊔ b) = a⊓ (a ⊔ b) = a⊔ b) = a
).
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≤ b
unfolds to a ⊔ b = b⊔ b = b
; cf. sup_eq_right
.
Equations
- One or more equations did not get rendered due to their size.
Distributivity laws #
Distributive lattices #
The infimum distributes over the supremum
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)⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)⊔ z) ≤ x ⊔ (y ⊓ z)≤ x ⊔ (y ⊓ z)⊔ (y ⊓ z)⊓ 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.
Instances
Equations
- OrderDual.distribLattice α = let src := inferInstanceAs (Lattice αᵒᵈ); DistribLattice.mk (_ : ∀ (x x_1 x_2 : αᵒᵈ), (x ⊔ x_1) ⊓ (x ⊔ x_2) ≤ x ⊔ x_1 ⊓ x_2)
Lattices derived from linear orders #
A lattice with total order is a linear order.
See note [reducible non-instances].
Equations
- Lattice.toLinearOrder α = let src := inst; LinearOrder.mk (_ : ∀ (a b : α), a ≤ b ∨ b ≤ a) inst inst inst
Equations
- instDistribLattice = let src := inferInstanceAs (Lattice α); DistribLattice.mk (_ : ∀ (x b c : α), (x ⊔ b) ⊓ (x ⊔ c) ≤ x ⊔ b ⊓ c)
Equations
- instDistribLatticeNat = inferInstance
Dual order #
Function lattices #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Monotone functions and lattices #
Pointwise supremum of two monotone functions is a monotone function.
Pointwise infimum of two monotone functions is a monotone function.
Pointwise maximum of two monotone functions is a monotone function.
Pointwise minimum of two monotone functions is a monotone function.
Pointwise supremum of two antitone functions is a antitone function.
Pointwise infimum of two antitone functions is a antitone function.
Pointwise maximum of two antitone functions is a antitone function.
Pointwise minimum of two antitone functions is a antitone function.
Products of (semi-)lattices #
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Subtypes of (semi-)lattices #
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.
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.
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.
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.
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.
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.
A type endowed with ⊔⊔
and ⊓⊓
is a DistribLattice
, if it admits an injective map that
preserves ⊔⊔
and ⊓⊓
to a DistribLattice
.
See note [reducible non-instances].
Equations
- One or more equations did not get rendered due to their size.
Equations
- instDistribLatticeBool = inferInstance