prop_iterationFunctor_map_succ — Mathlib

English

If j is not maximal, then the image under iterationFunctor map along le_succ lands in Φ.prop: Φ.prop ( (Φ.iterationFunctor J).map (homOfLE (Order.le_succ j)) ).

Русский

Если j не максимален, то изображение отображения вдоль le_succ через iterationFunctor лежит в Φ.prop.

LaTeX

$$$\\Phi.prop ((Φ.iterationFunctor J).map (homOfLE (Order.le_succ j)))$$$

Lean4

theorem prop_iterationFunctor_map_succ (j : J) (hj : ¬IsMax j) :
    Φ.prop ((Φ.iterationFunctor J).map (homOfLE (Order.le_succ j))) :=
  (Φ.transfiniteCompositionOfShapeιIteration J).map_mem j hj

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