Commit 2026-03-23 19:49 cd20542a

View on Github →

chore(CategoryTheory/Limits): functoriality of coconeLeftOpOfCone and co (#36918)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Cones.lean

added def CategoryTheory.Limits.coconeLeftOpOfConeEquiv

added def CategoryTheory.Limits.coconeRightOpOfConeEquiv

added def CategoryTheory.Limits.coconeUnopOfConeEquiv

added def CategoryTheory.Limits.coneLeftOpOfCoconeEquiv

added def CategoryTheory.Limits.coneOpEquiv

added def CategoryTheory.Limits.coneRightOpOfCoconeEquiv

added def CategoryTheory.Limits.coneUnopOfCoconeEquiv