Theorem CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShape

Modification history

2025-10-27 09:15
Mathlib/CategoryTheory/Limits/MorphismProperty.lean
refactor(CategoryTheory/ObjectProperty): IsClosedUnderLimitsOfShape (#29881) …
Deleted CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShapeView on Github →
2025-10-02 15:01
Mathlib/CategoryTheory/Limits/MorphismProperty.lean
feat(CategoryTheory/Limits/MorphismProperty): dualise lemmas on limits (#30127) …
Added CategoryTheory.MorphismProperty.Comma.hasColimitsOfShape_of_closedUnderColimitsOfShapeView on Github →