transfiniteIterate — Mathlib

English

Define the j-th iterate of a function φ: I → I along a well-ordered index J using transfinite recursion: at the base, at successors, and at limits via suprema.

Русский

Определим j-ю итерацию функции φ: I → I вдоль хорошо упорядоченного индекса J с помощью трансфинитной рекурсии: базовый случай, переходы по следующим шагам и пределы через супремумы.

LaTeX

$$$\\text{transfiniteIterate}_j(i) = \\begin{cases} i, & j = \\bot \\\\ φ(\\text{transfiniteIterate}_{j}(i)), & j \\text{ — successor} \\\\ \\bigvee_{x

Lean4

/-- The `j`th-iteration of a function `φ : I → I` when `j : J` belongs to
a well-ordered type. -/
noncomputable def transfiniteIterate (j : J) : I → I :=
  SuccOrder.limitRecOn j (fun _ _ ↦ id) (fun _ _ g ↦ φ ∘ g) (fun y _ h ↦ ⨆ (x : Set.Iio y), h x.1 x.2)

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