Commit 2023-03-13 12:32 ec210bab

View on Github →

feat: port CategoryTheory.Limits.Preserves.Opposites (#2826)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Limits.perservesColimitsOp

added def CategoryTheory.Limits.preservesColimitLeftOp

added def CategoryTheory.Limits.preservesColimitOp

added def CategoryTheory.Limits.preservesColimitRightOp

added def CategoryTheory.Limits.preservesColimitUnop

added def CategoryTheory.Limits.preservesColimitsLeftOp

added def CategoryTheory.Limits.preservesColimitsOfShapeLeftOp

added def CategoryTheory.Limits.preservesColimitsOfShapeOp

added def CategoryTheory.Limits.preservesColimitsOfShapeRightOp

added def CategoryTheory.Limits.preservesColimitsOfShapeUnop

added def CategoryTheory.Limits.preservesColimitsRightOp

added def CategoryTheory.Limits.preservesColimitsUnop

added def CategoryTheory.Limits.preservesFiniteColimitsLeftOp

added def CategoryTheory.Limits.preservesFiniteColimitsOp

added def CategoryTheory.Limits.preservesFiniteColimitsRightOp

added def CategoryTheory.Limits.preservesFiniteColimitsUnop

added def CategoryTheory.Limits.preservesFiniteLimitsLeftOp

added def CategoryTheory.Limits.preservesFiniteLimitsOp

added def CategoryTheory.Limits.preservesFiniteLimitsRightOp

added def CategoryTheory.Limits.preservesFiniteLimitsUnop

added def CategoryTheory.Limits.preservesLimitLeftOp

added def CategoryTheory.Limits.preservesLimitOp

added def CategoryTheory.Limits.preservesLimitRightOp

added def CategoryTheory.Limits.preservesLimitUnop

added def CategoryTheory.Limits.preservesLimitsLeftOp

added def CategoryTheory.Limits.preservesLimitsOfShapeLeftOp

added def CategoryTheory.Limits.preservesLimitsOfShapeOp

added def CategoryTheory.Limits.preservesLimitsOfShapeRightOp

added def CategoryTheory.Limits.preservesLimitsOfShapeUnop

added def CategoryTheory.Limits.preservesLimitsOp

added def CategoryTheory.Limits.preservesLimitsRightOp

added def CategoryTheory.Limits.preservesLimitsUnop