mathlib

a54dd9e3 - feat(order/category/BoundedDistribLattice): The category of bounded distributive lattices (#12347)

feat(order/category/BoundedDistribLattice): The category of bounded distributive lattices (#12347) Define `BoundedDistribLattice`, the category of bounded distributive lattices with bounded lattice homomorphisms.