Def CategoryTheory.Limits.evaluationJointlyReflectsColimits

Modification history

2026-10-31 10:05
Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
refactor(CategoryTheory): colimits of representable presheaves (#42816) …
Deleted CategoryTheory.Limits.evaluationJointlyReflectsColimitsView on Github →
2023-03-02 11:55
Mathlib/CategoryTheory/Limits/FunctorCategory.lean
feat: port/CategoryTheory.Limits.FunctorCategory (#2380)
Added CategoryTheory.Limits.evaluationJointlyReflectsColimitsView on Github →