transfiniteIterate_succ — Mathlib

English

If j is not the maximal element, the j+1-th iterate equals φ applied to the j-th iterate.

Русский

Если j не максимальный элемент, то j+1-я итерация равна применению φ к j-й итерации.

LaTeX

$$$\\text{transfiniteIterate}_{\\text{succ } j}(i_0) = φ(\\text{transfiniteIterate}_j(i_0))$ при условии $¬\\text{IsMax } j$$$

Lean4

theorem transfiniteIterate_succ (i₀ : I) (j : J) (hj : ¬IsMax j) :
    transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀) :=
  by
  dsimp [transfiniteIterate]
  rw [SuccOrder.limitRecOn_succ_of_not_isMax _ _ _ hj]
  rfl

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