Mathlib Changelog
v4
Changelog
About
Github
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