Theorem CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimit

Modification history

2024-11-03 13:44
Mathlib/CategoryTheory/Limits/Shapes/Grothendieck.lean
feat(CategoryTheory): Colimits on the Grothendieck construction (#18442) …
Added CategoryTheory.Limits.hasColimit_of_hasColimit_fiberwiseColimit_of_hasColimitView on Github →