Commit 2023-03-07 15:45 1c5ed784

View on Github →

feat: port CategoryTheory.Limits.Preserves.Shapes.Products (#2656)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean

added theorem CategoryTheory.Limits.PreservesCoproduct.inv_hom

added def CategoryTheory.Limits.PreservesCoproduct.iso

added def CategoryTheory.Limits.PreservesCoproduct.ofIsoComparison

added def CategoryTheory.Limits.PreservesProduct.iso

added theorem CategoryTheory.Limits.PreservesProduct.iso_hom

added def CategoryTheory.Limits.PreservesProduct.ofIsoComparison

added def CategoryTheory.Limits.isColimitCofanMkObjOfIsColimit

added def CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv

added def CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit

added def CategoryTheory.Limits.isColimitOfIsColimitCofanMkObj

added def CategoryTheory.Limits.isLimitFanMkObjOfIsLimit

added def CategoryTheory.Limits.isLimitMapConeFanMkEquiv

added def CategoryTheory.Limits.isLimitOfHasProductOfPreservesLimit

added def CategoryTheory.Limits.isLimitOfIsLimitFanMkObj