Commit 2023-04-05 15:22 41bcd06b

View on Github →

feat: port Order.Category.NonemptyFinLinOrd (#3282)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/NonemptyFinLinOrdCat.lean

added def NonemptyFinLinOrdCat.Iso.mk

added theorem NonemptyFinLinOrdCat.coe_of

added def NonemptyFinLinOrdCat.dual

added def NonemptyFinLinOrdCat.dualEquiv

added theorem NonemptyFinLinOrdCat.epi_iff_surjective

added theorem NonemptyFinLinOrdCat.forget_map_apply

added theorem NonemptyFinLinOrdCat.mono_iff_injective

added def NonemptyFinLinOrdCat.of

added def NonemptyFinLinOrdCat

added theorem nonemptyFinLinOrdCat_dual_comp_forget_to_linOrdCat