Theorem CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc

Modification history

2026-01-26 16:58

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

chore(CategoryTheory/Limits): add `IsColimit.nonempty_isColimit_iff_isIso_desc` and golf (#34237) …

Added CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc View on Github →