Commit 2024-11-30 09:05 c73ab4cd

View on Github →

feat(CategoryTheory/SmallObject/Iteration): existence of objects (bot and succ cases) (#19047)

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Functor.extendToSucc.map

added theorem CategoryTheory.Functor.extendToSucc.map_comp

added theorem CategoryTheory.Functor.extendToSucc.map_eq

added theorem CategoryTheory.Functor.extendToSucc.map_id

added theorem CategoryTheory.Functor.extendToSucc.map_self_succ

added def CategoryTheory.Functor.extendToSucc.obj

added def CategoryTheory.Functor.extendToSucc.objIso

added def CategoryTheory.Functor.extendToSucc.objSuccIso

added def CategoryTheory.Functor.extendToSucc

added def CategoryTheory.Functor.extendToSuccObjIso

added theorem CategoryTheory.Functor.extendToSuccObjIso_hom_naturality

added def CategoryTheory.Functor.extendToSuccObjSuccIso

added def CategoryTheory.Functor.extendToSuccRestrictionLEIso

added theorem CategoryTheory.Functor.extendToSucc_map_le_succ

added theorem CategoryTheory.Functor.extentToSucc_map

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

added def CategoryTheory.Functor.Iteration.mkOfBot