Theorem CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc

Modification history

2026-06-23 12:20

Mathlib/CategoryTheory/Limits/IsLimit.lean

feat(CategoryTheory/Limits/IsLimit): use `to_dual` on `IsLimit` (#36572) …

Deleted CategoryTheory.Limits.IsColimit.nonempty_isColimit_iff_isIso_desc View on Github →

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.IsColimit.nonempty_isColimit_iff_isIso_desc View on Github →