# mathlibdocumentation

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.

structure BoundedDistribLattice  :
Type (u_1+1)

The category of bounded distributive lattices with bounded lattice morphisms.

Instances for BoundedDistribLattice
@[protected, instance]
Equations
@[protected, instance]
Equations

Construct a bundled BoundedDistribLattice from a bounded_order distrib_lattice.

Equations
@[simp]
theorem BoundedDistribLattice.coe_of (α : Type u_1)  :
@[protected, instance]
Equations

Turn a BoundedDistribLattice into a BoundedLattice by forgetting it is distributive.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]

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

Equations

order_dual as a functor.

Equations
@[simp]
@[simp]

The equivalence between BoundedDistribLattice and itself induced by order_dual both ways.

Equations