Def CategoryTheory.Functor.Iteration.mkOfBot

Modification history

2024-11-30 09:05

Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean

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

Added CategoryTheory.Functor.Iteration.mkOfBot View on Github →