Commit 2024-10-03 17:44 78d98550

View on Github →

feat(CategoryTheory/Limits): Some infrastructure for the preservation of finite (co)limits (#17156)

Estimated changes

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

added def CategoryTheory.Limits.preservesFiniteColimitsOfNatIso

added def CategoryTheory.Limits.preservesFiniteLimitsOfNatIso

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

added def CategoryTheory.preservesFiniteColimitsOfEvaluation

added def CategoryTheory.preservesFiniteLimitsOfEvaluation