instIsIsoRightAppArrowιIteration

English

For any j₁, j₂ in κ.ord.toType and morphism φ: j₁ ⟶ j₂, and any f : Arrow C, the right component of ((iterationFunctor I κ).map φ).app f is an isomorphism.

Русский

Для любых j₁, j₂ в κ.ord.toType и морфизма φ: j₁ ⟶ j₂, и любого f : Arrow C правый компонент ((iterationFunctor I κ).map φ).app f является изоморфизмом.

LaTeX

$$$\\forall j_1,j_2:\\kappa.ord.toType,\\; φ:\\bigl(j_1\\to j_2\\bigr),\\; f:\\mathrm{Arrow}(C),\\; IsIso\\Bigl(((\\text{iterationFunctor}(I,\\kappa).\\mathrm{map}\\;φ).\\mathrm{app} f)\\Bigr).\\mathrm{right}$$$

Lean4

instance (f : Arrow C) : IsIso ((ιIteration I κ).app f).right :=
  (transfiniteCompositionOfShapeιIterationAppRight I κ f).isIso

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