Commit 2022-03-04 17:34 a54dd9e3

View on Github →

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

Estimated changes

Created src/order/category/BoundedDistribLattice.lean

added theorem BoundedDistribLattice.coe_of

added theorem BoundedDistribLattice.coe_to_BoundedLattice

added def BoundedDistribLattice.dual

added def BoundedDistribLattice.dual_equiv

added theorem BoundedDistribLattice.forget_BoundedLattice_Lattice_eq_forget_DistribLattice_Lattice

added def BoundedDistribLattice.iso.mk

added def BoundedDistribLattice.of

added def BoundedDistribLattice.to_BoundedLattice

added structure BoundedDistribLattice

added theorem BoundedDistribLattice_dual_comp_forget_to_DistribLattice

Modified src/order/category/DistribLattice.lean