Commit 2023-03-06 11:42 d1ee6c39

View on Github →

feat: port CategoryTheory.Limits.Preserves.Finite (#2648)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Category/ULift.lean

modified def CategoryTheory.ULiftHom.{w,u}

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

added def CategoryTheory.Limits.compPreservesFiniteColimits

added def CategoryTheory.Limits.compPreservesFiniteLimits

added def CategoryTheory.Limits.preservesFiniteColimitsOfPreservesFiniteColimitsOfSize

added def CategoryTheory.Limits.preservesFiniteLimitsOfPreservesFiniteLimitsOfSize