Theorem CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_lift

Modification history

2026-01-26 16:58
Mathlib/CategoryTheory/Limits/IsLimit.lean
chore(CategoryTheory/Limits): add `IsColimit.nonempty_isColimit_iff_isIso_desc` and golf (#34237) …
Added CategoryTheory.Limits.IsLimit.nonempty_isLimit_iff_isIso_liftView on Github →