Commit 2025-12-01 17:54 f707e36d

View on Github →

feat(CategoryTheory): improve API for limits in preorders (#32178)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preorder.lean

added def Preorder.coconeOfUpperBound

added theorem Preorder.coconePt_mem_upperBounds

deleted def Preorder.coconePt_mem_upperBounds

added def Preorder.colimitCoconeOfIsLUB

modified theorem Preorder.hasLimit_iff_hasGLB

added def Preorder.limitConeOfIsGLB

deleted theorem Preorder.upperBoundOfCocone