Commit 2023-04-05 11:30 c84577c5

View on Github →

feat: port Order.Category.PartOrd (#3266)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/PartOrdCat.lean

added def PartOrdCat.Iso.mk

added theorem PartOrdCat.coe_of

added def PartOrdCat.dual

added def PartOrdCat.dualEquiv

added def PartOrdCat.of

added def PartOrdCat

added theorem partOrdCat_dual_comp_forget_to_preordCat

added def preordCatToPartOrdCat

added def preordCatToPartOrdCatCompToDualIsoToDualCompPreordCatToPartOrdCat

added def preordCatToPartOrdCatForgetAdjunction