iterationFunctorMapSuccAppArrowIso_hom_left

English

For any f : Arrow C, the right-hand morphism of ((ιIteration I κ).app f).right is an isomorphism.

Русский

Для любого f : Arrow C правая часть морфизма ((ιIteration I κ).app f).right является изоморфизмом.

LaTeX

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

Lean4

@[simp]
theorem iterationFunctorMapSuccAppArrowIso_hom_left (f : Arrow C) (j : κ.ord.toType) :
    (iterationFunctorMapSuccAppArrowIso I κ f j).hom.left = 𝟙 _ :=
  rfl

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