Commit 2023-03-02 21:38 04fa3d33

View on Github →

feat: port CategoryTheory.Limits.Preserves.Shapes.Terminal (#2579)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.IsInitial.isInitialObj

added def CategoryTheory.Limits.IsInitial.isInitialOfObj

added def CategoryTheory.Limits.IsTerminal.isTerminalObj

added def CategoryTheory.Limits.IsTerminal.isTerminalOfObj

added def CategoryTheory.Limits.PreservesInitial.iso

added theorem CategoryTheory.Limits.PreservesInitial.iso_hom

added def CategoryTheory.Limits.PreservesInitial.ofIsoComparison

added def CategoryTheory.Limits.PreservesTerminal.iso

added theorem CategoryTheory.Limits.PreservesTerminal.iso_hom

added def CategoryTheory.Limits.PreservesTerminal.ofIsoComparison

added theorem CategoryTheory.Limits.hasInitial_of_hasInitial_of_preservesColimit

added theorem CategoryTheory.Limits.hasTerminal_of_hasTerminal_of_preservesLimit

added def CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv

added def CategoryTheory.Limits.isColimitOfHasInitialOfPreservesColimit

added def CategoryTheory.Limits.isLimitMapConeEmptyConeEquiv

added def CategoryTheory.Limits.isLimitOfHasTerminalOfPreservesLimit

added def CategoryTheory.Limits.preservesColimitsOfShapePemptyOfPreservesInitial

added def CategoryTheory.Limits.preservesInitialOfIsIso

added def CategoryTheory.Limits.preservesInitialOfIso

added def CategoryTheory.Limits.preservesLimitsOfShapePemptyOfPreservesTerminal

added def CategoryTheory.Limits.preservesTerminalOfIsIso

added def CategoryTheory.Limits.preservesTerminalOfIso