Commit 2023-06-13 07:27 de8ac50a

View on Github →

feat: port Order.Category.BddOrdCat (#4984)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Category/BddOrdCat.lean

added def BddOrdCat.Iso.mk

added theorem BddOrdCat.coe_of

added def BddOrdCat.dual

added def BddOrdCat.dualEquiv

added def BddOrdCat.of

added structure BddOrdCat

added theorem bddOrd_dual_comp_forget_to_bipointed

added theorem bddOrd_dual_comp_forget_to_partOrdCat