Theorem CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc

Modification history

2024-06-17 14:29
Mathlib/CategoryTheory/Limits/Shapes/Products.lean
feat(CategoryTheory): characterise the covering sieves for the extensive topology (#13897)
Added CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDescView on Github →