iterationObjRightIso — Mathlib

English

For any f : Arrow C, the right-hand component of the app under ιIteration is a transfinite composition of isomorphisms.

Русский

Для любого f : Arrow C правая часть приложения к ιIteration является трансфинитной композицией изоморфизмов.

LaTeX

$$$((\\iotaIteration I κ).app f).right :\\text{TransfiniteCompositionOfShape}(κ.ord.toType) \\, (\\operatorname{Isomorphisms}(C))$$$

Lean4

/-- For any `f : Arrow C`, the object `((iteration I κ).obj f).right`
identifies to `f.right`. -/
@[simps! hom]
noncomputable def iterationObjRightIso (f : Arrow C) : f.right ≅ ((iteration I κ).obj f).right :=
  asIso ((ιIteration I κ).app f).right

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