Commit 2023-03-01 18:09 8975880d

View on Github →

feat: port/CategoryTheory.Limits.Preserves.Limit (#2379)

Estimated changes

Modified Mathlib.lean

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

added theorem CategoryTheory.lift_comp_preservesLimitsIso_hom

added def CategoryTheory.preservesColimitIso

added def CategoryTheory.preservesColimitNatIso

added theorem CategoryTheory.preservesColimitsIso_inv_comp_desc

added def CategoryTheory.preservesLimitIso

added def CategoryTheory.preservesLimitNatIso

added theorem CategoryTheory.preservesLimitsIso_hom_π

added theorem CategoryTheory.preservesLimitsIso_inv_π

added theorem CategoryTheory.preserves_desc_mapCocone

added theorem CategoryTheory.preserves_lift_mapCone

added theorem CategoryTheory.ι_preservesColimitsIso_hom

added theorem CategoryTheory.ι_preservesColimitsIso_inv