iterationFunctorObjSuccIso — Mathlib

English

For non-max j there is an isomorphism between (Φ.iterationFunctor J).obj (Order.succ j) and Φ.succ ((Φ.iterationFunctor J).obj j).

Русский

Для не максимального j существует изоморфизм между (Φ.iterationFunctor J).obj (Order.succ j) и Φ.succ ((Φ.iterationFunctor J).obj j).

LaTeX

$$$ (Φ.iterationFunctor J).obj (Order.succ j) \\cong Φ.succ ((Φ.iterationFunctor J).obj j) $$$

Lean4

/-- When `j` is not a maximal element, then
`(Φ.iterationFunctor J).obj (Order.succ j)` is isomorphic to
`Φ.succ ((Φ.iterationFunctor J).obj j)`. -/
noncomputable def iterationFunctorObjSuccIso (j : J) (hj : ¬IsMax j) :
    (Φ.iterationFunctor J).obj (Order.succ j) ≅ Φ.succ ((Φ.iterationFunctor J).obj j) :=
  eqToIso ((Φ.prop_iterationFunctor_map_succ j hj).succ_eq.symm)

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