isColimitIterationCocone — Mathlib

English

The iteration cocone is a colimit cocone for the iteration functor.

Русский

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

LaTeX

$$$\\mathrm{isColimitIterationCocone} : \\mathrm{IsColimit}(Φ.iterationCocone J)$$$

Lean4

/-- `Φ.iteration J` identifies to the colimit of `Φ.iterationFunctor J`. -/
noncomputable def isColimitIterationCocone : IsColimit (Φ.iterationCocone J) :=
  colimit.isColimit _

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