Theorem CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit'

Modification history

2024-11-25 15:15

Mathlib/CategoryTheory/Limits/Constructions/EventuallyConstant.lean

feat(CategoryTheory): limits of eventually constant functors from cofiltered categories (#19021) …

Added CategoryTheory.Functor.IsEventuallyConstantFrom.isIso_ι_of_isColimit'View on Github →