iterationCocone_pt

Mathlib.CategoryTheory.SmallObject.TransfiniteIteration

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

English

The point of the iteration cocone equals the iteration object.

Русский

Точка коконета итерации равна объекту итерации.

LaTeX

$$$Φ.iterationCocone J .\\mathrm{pt} = Φ.iteration J$$$

Lean4

@[simp]
theorem iterationCocone_pt : (Φ.iterationCocone J).pt = Φ.iteration J :=
  rfl

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

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

Разделы

Аффилиация

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