toSuccArrow

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.SuccStruct.toSuccArrow

Lean4

/-- The map `Φ.toSucc X : X ⟶ Φ.Succ X`, as an element in `Arrow C`. -/
@[simps!]
def toSuccArrow (X : C) : Arrow C :=
  Arrow.mk (Φ.toSucc X)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru