Commit 2024-03-24 10:44 ffd40253

View on Github →

chore: rename lemmas involving closedUnder{Co}limits (#11608) They contain a hypothesis ClosedUnder{Co}Limits, hence should be named accordingly.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/FullSubcategory.lean

added theorem CategoryTheory.Limits.hasColimit_of_closedUnderColimits

deleted theorem CategoryTheory.Limits.hasColimit_of_closed_under_colimits

added theorem CategoryTheory.Limits.hasColimitsOfShape_of_closedUnderColimits

deleted theorem CategoryTheory.Limits.hasColimitsOfShape_of_closed_under_colimits

added theorem CategoryTheory.Limits.hasLimit_of_closedUnderLimits

deleted theorem CategoryTheory.Limits.hasLimit_of_closed_under_limits

added theorem CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits

deleted theorem CategoryTheory.Limits.hasLimitsOfShape_of_closed_under_limits