Commit 2024-11-11 12:27 7f8c9acc

View on Github →

chore: dualize Limits.Preserves.Opposites (#18814)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

added def CategoryTheory.Limits.isColimitOfOp

added def CategoryTheory.Limits.isColimitOfUnop

added def CategoryTheory.Limits.isLimitOfOp

added def CategoryTheory.Limits.isLimitOfUnop

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added def CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone

added def CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp

added def CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp

added def CategoryTheory.Limits.isColimitOfConeOfCoconeUnop

added def CategoryTheory.Limits.isColimitOfConeRightOpOfCocone

added def CategoryTheory.Limits.isColimitOfConeUnopOfCocone

added def CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone

added def CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp

added def CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp

added def CategoryTheory.Limits.isLimitOfCoconeOfConeUnop

added def CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone

added def CategoryTheory.Limits.isLimitOfCoconeUnopOfCone

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

added def CategoryTheory.Limits.preservesColimitOfLeftOp

added def CategoryTheory.Limits.preservesColimitOfOp

added def CategoryTheory.Limits.preservesColimitOfRightOp

added def CategoryTheory.Limits.preservesColimitOfUnop

added def CategoryTheory.Limits.preservesColimitsOfLeftOp

added def CategoryTheory.Limits.preservesColimitsOfOp

added def CategoryTheory.Limits.preservesColimitsOfRightOp

added def CategoryTheory.Limits.preservesColimitsOfShapeOfLeftOp

added def CategoryTheory.Limits.preservesColimitsOfShapeOfOp

added def CategoryTheory.Limits.preservesColimitsOfShapeOfRightOp

added def CategoryTheory.Limits.preservesColimitsOfShapeOfUnop

added def CategoryTheory.Limits.preservesColimitsOfSizeLeftOp

added def CategoryTheory.Limits.preservesColimitsOfSizeOfLeftOp

added def CategoryTheory.Limits.preservesColimitsOfSizeOfOp

added def CategoryTheory.Limits.preservesColimitsOfSizeOfRightOp

added def CategoryTheory.Limits.preservesColimitsOfSizeOfUnop

added def CategoryTheory.Limits.preservesColimitsOfSizeOp

added def CategoryTheory.Limits.preservesColimitsOfSizeRightOp

added def CategoryTheory.Limits.preservesColimitsOfSizeUnop

added def CategoryTheory.Limits.preservesColimitsOfUnop

added def CategoryTheory.Limits.preservesFiniteColimitsOfLeftOp

added def CategoryTheory.Limits.preservesFiniteColimitsOfOp

added def CategoryTheory.Limits.preservesFiniteColimitsOfRightOp

added def CategoryTheory.Limits.preservesFiniteColimitsOfUnop

added def CategoryTheory.Limits.preservesFiniteLimitsOfLeftOp

added def CategoryTheory.Limits.preservesFiniteLimitsOfOp

added def CategoryTheory.Limits.preservesFiniteLimitsOfRightOp

added def CategoryTheory.Limits.preservesFiniteLimitsOfUnop

added def CategoryTheory.Limits.preservesLimitOfLeftOp

added def CategoryTheory.Limits.preservesLimitOfOp

added def CategoryTheory.Limits.preservesLimitOfRightOp

added def CategoryTheory.Limits.preservesLimitOfUnop

added def CategoryTheory.Limits.preservesLimitsOfLeftOp

added def CategoryTheory.Limits.preservesLimitsOfOp

added def CategoryTheory.Limits.preservesLimitsOfRightOp

added def CategoryTheory.Limits.preservesLimitsOfShapeOfLeftOp

added def CategoryTheory.Limits.preservesLimitsOfShapeOfOp

added def CategoryTheory.Limits.preservesLimitsOfShapeOfRightOp

added def CategoryTheory.Limits.preservesLimitsOfShapeOfUnop

added def CategoryTheory.Limits.preservesLimitsOfSizeLeftOp

added def CategoryTheory.Limits.preservesLimitsOfSizeOfLeftOp

added def CategoryTheory.Limits.preservesLimitsOfSizeOfOp

added def CategoryTheory.Limits.preservesLimitsOfSizeOfRightOp

added def CategoryTheory.Limits.preservesLimitsOfSizeOfUnop

added def CategoryTheory.Limits.preservesLimitsOfSizeOp

added def CategoryTheory.Limits.preservesLimitsOfSizeRightOp

added def CategoryTheory.Limits.preservesLimitsOfSizeUnop

added def CategoryTheory.Limits.preservesLimitsOfUnop