Commit 2026-05-20 14:58 70277a11

View on Github →

chore(CategoryTheory/Limits): preservation of pullbacks in terms of IsPullback (#39595)

Estimated changes

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

added theorem CategoryTheory.Limits.PreservesColimit.mk'

added theorem CategoryTheory.Limits.PreservesLimit.mk'

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

added theorem CategoryTheory.IsPullback.preservesLimit_cospan_iff

added theorem CategoryTheory.IsPushout.preservesColimit_span_iff

added theorem CategoryTheory.Limits.preservesColimitsOfShape_walkingCospan_of_forall_isPushout

added theorem CategoryTheory.Limits.preservesLimitsOfShape_walkingCospan_of_forall_isPullback