iter — Mathlib

English

The SuccStruct iteration and its objects are defined: iter, the iteration functor, the iteration cocone, and the iteration object itself via colimits.

Русский

Определены операции итерации SuccStruct: iter, iterationFunctor, iterationCocone и сам объект итерации через колимит.

LaTeX

$$$$ \text{iterationFunctor}, \text{iterationCocone}, \text{iteration} = \operatorname{colim} (\text{iterationFunctor}) $$$$

Lean4

/-- Given `Φ : SuccStruct C` and an element `j : J` in a well-ordered type,
this is the unique element in `Φ.Iteration j`. -/
noncomputable def iter (j : J) : Φ.Iteration j :=
  Classical.arbitrary _

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