Commit 2024-11-10 22:20 9041e9d5

View on Github →

feat(CategoryTheory/SmallObject/Iteration): the unique morphism (bot and succ cases) (#18127)

Estimated changes

Modified Mathlib.lean

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

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

added def CategoryTheory.Functor.Iteration.Hom.mkOfBot

added theorem CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp_eq_of_le

added theorem CategoryTheory.Functor.Iteration.Hom.mkOfSuccNatTransApp_succ_eq