prop_iterationFunctor_map_succ — Mathlib

English

For any j, the succ map along j has the property asserted by succStruct in the iteration functor.

Русский

Для любого j отображение succ на J обладает свойством, соответствующим succStruct для итерационного функторa.

LaTeX

$$$\\text{prop\\_iterationFunctor\\_map\\_succ}(I,\\kappa; j)$$$

Lean4

theorem prop_iterationFunctor_map_succ (j : κ.ord.toType) :
    (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE (Order.le_succ j))) :=
  by
  have := hasIterationOfShape I κ
  have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
  exact (succStruct I κ).prop_iterationFunctor_map_succ j (not_isMax j)

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