Theorem CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift

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.Fan.nonempty_isLimit_iff_isIso_piLiftView on Github →