Commit 2024-11-14 20:13 a692b479

View on Github →

feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limit case) (#18137)

Estimated changes

Modified Mathlib/CategoryTheory/SmallObject/Iteration/UniqueHom.lean

added def CategoryTheory.Functor.Iteration.Hom.mkOfLimit

added def CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTrans

added def CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp

added theorem CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_eq_of_lt

added theorem CategoryTheory.Functor.Iteration.Hom.mkOfLimitNatTransApp_naturality_top

added theorem CategoryTheory.Functor.Iteration.iso_refl

added theorem CategoryTheory.Functor.Iteration.iso_trans