Commit 2022-03-01 02:55 cd98967d

View on Github →

feat(order/category/CompleteLattice): The category of complete lattices (#12348) Define CompleteLattice, the category of complete lattices with complete lattice homomorphisms.

Estimated changes

Created src/order/category/CompleteLattice.lean

added def CompleteLattice.dual

added def CompleteLattice.dual_equiv

added def CompleteLattice.iso.mk

added def CompleteLattice.of

added def CompleteLattice

added theorem CompleteLattice_dual_comp_forget_to_BoundedLattice

Modified src/order/hom/complete_lattice.lean

added def complete_lattice_hom.to_bounded_lattice_hom