Commit 2023-05-08 06:19 937b1c59

View on Github →

feat(order/category): Category of finite distributive lattices (#11677) Define FinBddDistLat, the category of finite distributive lattices with bounded lattice homomorphisms. This is one of the two categories involved in Birkhoff's representation theorem.

Estimated changes

Created src/order/category/FinBddDistLat.lean

added def FinBddDistLat.dual

added def FinBddDistLat.dual_equiv

added def FinBddDistLat.iso.mk

added def FinBddDistLat.of'

added def FinBddDistLat.of

added structure FinBddDistLat

added theorem FinBddDistLat_dual_comp_forget_to_BddDistLat

Modified src/order/category/FinBoolAlg.lean

added theorem FinBoolAlg_dual_comp_forget_to_FinBddDistLat

Modified src/order/category/FinPartOrd.lean