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