mathlib documentation

order.category.BoundedDistribLattice

The category of bounded distributive lattices #

This defines BoundedDistribLattice, the category of bounded distributive lattices.

Note that this category is sometimes called DistLat when being a lattice is understood to entail having a bottom and a top element.

@[protected, instance]
Equations

Constructs an equivalence between bounded distributive lattices from an order isomorphism between them.

Equations

order_dual as a functor.

Equations