Commit 2022-02-26 23:31 817b4c4b

View on Github →

feat(order/category/BoundedLattice): The category of bounded lattices (#12257) Define BoundedLattice, the category of bounded lattices with bounded lattice homs.

Estimated changes

Created src/order/category/BoundedLattice.lean

added def BoundedLattice.dual

added def BoundedLattice.dual_equiv

added theorem BoundedLattice.forget_Lattice_PartialOrder_eq_forget_BoundedOrder_PartialOrder

added def BoundedLattice.iso.mk

added def BoundedLattice.of

added structure BoundedLattice

added theorem BoundedLattice_dual_comp_forget_to_BoundedOrder

added theorem BoundedLattice_dual_comp_forget_to_Lattice

Modified src/order/hom/lattice.lean