Theorem CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_eq_of_lt

Modification history

2025-02-03 20:04
Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
refactor(CategoryTheory/SmallObject): generalization of the definitions (#20256) …
Deleted CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_eq_of_ltView on Github →
2024-11-14 20:13
Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case) (#18137)
Added CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_eq_of_ltView on Github →