Commit 2023-04-05 08:46 bdfb716a

View on Github →

feat: port Order.Category.Preord (#3265)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/PreordCat.lean

added def PreordCat.Iso.mk

added theorem PreordCat.coe_of

added def PreordCat.dual

added def PreordCat.dualEquiv

added def PreordCat.of

added def PreordCat

added def preordCatToCat