transfiniteIterate_limit — Mathlib

English

At a limit index j, the j-th iterate is the supremum of all previous iterates.

Русский

При пределе индекса j j-я итерация равна верхней границе всех предыдущих итераций.

LaTeX

$$$\\text{transfiniteIterate}_j(i_0) = \\bigvee_{x

Lean4

theorem transfiniteIterate_limit (i₀ : I) (j : J) (hj : Order.IsSuccLimit j) :
    transfiniteIterate φ j i₀ = ⨆ (x : Set.Iio j), transfiniteIterate φ x.1 i₀ :=
  by
  dsimp [transfiniteIterate]
  rw [SuccOrder.limitRecOn_of_isSuccLimit _ _ _ hj]
  simp only [iSup_apply]

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