Commit 2023-07-04 05:50 3aeae834

View on Github →

chore: dualize statements about pullbacks to pushouts (#5700)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

added def CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv

added def CategoryTheory.Limits.WidePushoutShape.uliftEquivalence

added theorem CategoryTheory.Limits.hasWidePushouts_shrink