Commit 2023-03-07 16:09 6a058b4c

View on Github →

feat: port/CategoryTheory.Limits.Shapes.FiniteLimits (#2647)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

added theorem CategoryTheory.Limits.hasFiniteColimits_of_hasFiniteColimits_of_size

added theorem CategoryTheory.Limits.hasFiniteLimits_of_hasFiniteLimits_of_size

added theorem CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits

added theorem CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits