Commit 2023-05-26 15:03 8828d20b

View on Github →

feat: port Order.Category.FinPartOrd (#3831)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/FinPartOrd.lean

added def FinPartOrd.Iso.mk

added theorem FinPartOrd.coe_of

added def FinPartOrd.dual

added def FinPartOrd.dualEquiv

added def FinPartOrd.of

added structure FinPartOrd

added theorem FinPartOrd_dual_comp_forget_to_partOrdCat