iterationFunctor — Mathlib

English

The functor iterationFunctor I κ is a functor from κ-ordered type to the endofunctor on Arrow C; it encodes the entire iterative process of succStruct I κ across the index κ.

Русский

Функтор итерации iterationFunctor I κ является функтором от κ-упорядоченного типа к концевому функтору на Arrow C; он кодирует весь процесс итерации succStruct I κ по индексу κ.

LaTeX

$$$\\text{iterationFunctor}:\\kappa.ord.toType \\to \\mathrm{Funct}(\\mathrm{Arrow}(C),\\mathrm{Arrow}(C))$$$

Lean4

/-- The functor `κ.ord.toType ⥤ Arrow C ⥤ Arrow C` corresponding to the
iterations of the successor structure `succStruct I κ`. -/
noncomputable def iterationFunctor : κ.ord.toType ⥤ Arrow C ⥤ Arrow C :=
  haveI := hasIterationOfShape I κ
  (succStruct I κ).iterationFunctor κ.ord.toType

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