Commit 2023-06-13 10:44 dc318ce8

View on Github →

feat: port Order.Category.SemilatCat (#4990)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/SemilatCat.lean

added def SemilatInfCat.Iso.mk

added theorem SemilatInfCat.coe_forget_to_partOrdCat

added theorem SemilatInfCat.coe_of

added def SemilatInfCat.dual

added def SemilatInfCat.of

added structure SemilatInfCat

added theorem SemilatInfCat_dual_comp_forget_to_partOrdCat

added def SemilatSupCat.Iso.mk

added theorem SemilatSupCat.coe_forget_to_partOrdCat

added theorem SemilatSupCat.coe_of

added def SemilatSupCat.dual

added def SemilatSupCat.of

added structure SemilatSupCat

added def SemilatSupCatEquivSemilatInfCat

added theorem SemilatSupCat_dual_comp_forget_to_partOrdCat