iterationCocone — Mathlib

English

The cocone Φ.iterationCocone J expresses that Φ.iteration J is the colimit of Φ.iterationFunctor J.

Русский

Кокон Φ.iterationCocone J выражает, что Φ.iteration J является колимитом Φ.iterationFunctor J.

LaTeX

$$$\\text{Φ.iterationCocone } J$ is a colimit cocone for $Φ.iterationFunctor J$.$$

Lean4

/-- The colimit cocone expressing that `Φ.iteration J` is the colimit
of `Φ.iterationFunctor J`. -/
noncomputable def iterationCocone : Cocone (Φ.iterationFunctor J) :=
  colimit.cocone _

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