transfiniteCompositionOfShapeιIterationAppRight

English

For any arrow f, the right-hand morphism of the app at f under ιIteration is an isomorphism.

Русский

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

LaTeX

$$$\\forall f,\\; IsIso\\Bigl(((\\iotaIteration I κ).app f).{\\text{right}}\\Bigr)$$$

Lean4

/-- For any `f : Arrow C`, the map `((ιIteration I κ).app f).right` is
a transfinite composition of isomorphisms. -/
noncomputable def transfiniteCompositionOfShapeιIterationAppRight (f : Arrow C) :
    (isomorphisms C).TransfiniteCompositionOfShape κ.ord.toType ((ιIteration I κ).app f).right :=
  haveI := hasIterationOfShape I κ
  let h := transfiniteCompositionOfShapeSuccStructPropιIteration I κ
  { toTransfiniteCompositionOfShape := h.toTransfiniteCompositionOfShape.map ((evaluation _ _).obj f ⋙ Arrow.rightFunc)
    map_mem j hj := ((succStruct_prop_le_propArrow I κ _ (h.map_mem j hj)) f).2 }

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