Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-15 14:39 77ca1ed3

View on Github →

feat(order/category/Lattice): The category of lattices (#11968) Define Lattice, the category of lattices with lattice homs.

Estimated changes

Modified src/category_theory/concrete_category/bundled_hom.lean

Created src/order/category/Lattice.lean

added def Lattice.dual

added def Lattice.dual_equiv

added def Lattice.iso.mk

added def Lattice.of

added def Lattice

added theorem Lattice_dual_comp_forget_to_PartialOrder

Modified src/order/category/LinearOrder.lean

added def LinearOrder.dual

deleted def LinearOrder.to_dual

added theorem LinearOrder_dual_comp_forget_to_Lattice

deleted theorem LinearOrder_dual_equiv_comp_forget_to_PartialOrder

Modified src/order/hom/lattice.lean