Commit 2023-03-06 07:28 c76cd45d

View on Github →

feat: port CategoryTheory.Limits.Preserves.Shapes.BinaryProduct (#2654)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.PreservesColimitPair.iso

added theorem CategoryTheory.Limits.PreservesColimitPair.iso_hom

added def CategoryTheory.Limits.PreservesColimitPair.ofIsoCoprodComparison

added def CategoryTheory.Limits.PreservesLimitPair.iso

added theorem CategoryTheory.Limits.PreservesLimitPair.iso_hom

added def CategoryTheory.Limits.PreservesLimitPair.ofIsoProdComparison

added def CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv

added def CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit

added def CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit

added def CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv

added def CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit

added def CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit

added def CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit

added def CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit