Def CategoryTheory.Functor.restrictionLTOfCoconeIso

Modification history

2025-02-03 20:04

Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …

Deleted CategoryTheory.Functor.restrictionLTOfCoconeIso View on Github →

2024-12-21 09:50

Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean

feat(CategoryTheory/SmallObject/Iteration): Functor.ofCocone (#19643) …

Added CategoryTheory.Functor.restrictionLTOfCoconeIso View on Github →