Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-14 20:20
34a3845a
View on Github →
feat: port Order.Category.CompleteLatCat (
#5019
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Order/Category/BddOrdCat.lean
Created
Mathlib/Order/Category/CompleteLatCat.lean
added
def
CompleteLatCat.Iso.mk
added
theorem
CompleteLatCat.coe_of
added
def
CompleteLatCat.dual
added
def
CompleteLatCat.dualEquiv
added
def
CompleteLatCat.of
added
def
CompleteLatCat
added
theorem
completeLatCat_dual_comp_forget_to_bddLatCat
Modified
Mathlib/Order/Category/SemilatCat.lean