English
The morphism ιIteration I κ is a transfinite composition of shape κ.ord.toType consisting of morphisms satisfying (succStruct I κ).prop.
Русский
Морфизм ιIteration I κ является трансфинитной композицией формы κ.ord.toType, состоящей из морфизмов, удовлетворяющих свойству (succStruct I κ).prop.
LaTeX
$$$\\text{ιIteration}: (\\text{succStruct}(I,\\kappa).\\text{prop}).\\text{TransfiniteCompositionOfShape}(\\kappa.ord.toType)$$$
Lean4
/-- The morphism `ιIteration I κ` is a transfinite composition of shape
`κ.ord.toType` of morphisms satisfying `(succStruct I κ).prop`. -/
noncomputable def transfiniteCompositionOfShapeSuccStructPropιIteration :
(succStruct I κ).prop.TransfiniteCompositionOfShape κ.ord.toType (ιIteration I κ) :=
haveI := hasIterationOfShape I κ
(succStruct I κ).transfiniteCompositionOfShapeιIteration κ.ord.toType
