Commit 2026-05-21 19:52 27850fe7

View on Github →

chore(Mathlib/CategoryTheory/Limits): add iff_of_natIso versions of variants of preservesLimits_of_natIso (#39667) ... as well as preservesLimit_iff_isLimit_mapCone: a functor preserves a limit if and only if it preserves some limit cone This PR was automatically created from PR #39572 by @chrisflav via a review comment by @dagurtomas.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Preserves/Basic.lean

added theorem CategoryTheory.Limits.preservesColimit_iff_isColimit_mapCocone

added theorem CategoryTheory.Limits.preservesColimit_iff_of_natIso

added theorem CategoryTheory.Limits.preservesColimitsOfShape_iff_of_natIso

added theorem CategoryTheory.Limits.preservesColimitsOfSize_iff_of_natIso

added theorem CategoryTheory.Limits.preservesLimit_iff_isLimit_mapCone

added theorem CategoryTheory.Limits.preservesLimit_iff_of_natIso

added theorem CategoryTheory.Limits.preservesLimitsOfShape_iff_of_natIso

added theorem CategoryTheory.Limits.preservesLimitsOfSize_iff_of_natIso