iteration — Mathlib

English

The construction iteration is the colimit of the successive applications of the successor structure along the index κ; it composes the chain of morphisms produced by succStruct.

Русский

Построение итерации является пределом-колимитом последовательного применения структуры-последовательности вдоль индекса κ; оно объединяет всю цепь морфизмов, порожденных succStruct.

LaTeX

$$$\\text{iteration}(I,\\kappa) = \\operatorname{colim}_{\\alpha<\\kappa} \\text{succStruct}^{\\alpha}(I,\\kappa)$$$

Lean4

/-- The colimit of `iterationFunctor I κ`. -/
noncomputable def iteration : Arrow C ⥤ Arrow C :=
  haveI := hasIterationOfShape I κ
  (succStruct I κ).iteration κ.ord.toType

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