Commit 2024-11-02 12:50 c46b5e46

View on Github →

chore: variants of hasLimit_of_hasColimit_leftOp (#18530) Also turns variants into global instances if this is safe.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/IndYoneda.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added theorem CategoryTheory.Limits.hasColimit_of_hasLimit_rightOp

added theorem CategoryTheory.Limits.hasColimit_of_hasLimit_unop

deleted theorem CategoryTheory.Limits.hasColimit_op_of_hasLimit

added theorem CategoryTheory.Limits.hasLimit_of_hasColimit_rightOp

added theorem CategoryTheory.Limits.hasLimit_of_hasColimit_unop

deleted theorem CategoryTheory.Limits.hasLimit_op_of_hasColimit

added def CategoryTheory.Limits.isColimitCoconeOfConeUnop

deleted def CategoryTheory.Limits.isColimitConeOfCoconeUnop