English
Same as above in a concise form for a single-parameter function over an index set.
Русский
То же самое в краткой форме для функции с индексами.
LaTeX
$$iInter {ι : Type u} {f : ι → Set Ordinal} {o : Ordinal} (h : ∀ i, IsClosedBelow (f i) o) : IsClosedBelow (Set.iInter fun i => f i) o$$
Lean4
/-- `veblenWith f o` is the `o`-th function in the Veblen hierarchy starting with `f`. This is
defined so that
- `veblenWith f 0 = f`.
- `veblenWith f o` for `o ≠ 0` enumerates the common fixed points of `veblenWith f o'` over all
`o' < o`.
-/
@[pp_nodot]
def veblenWith (f : Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u} → Ordinal.{u} :=
if o = 0 then f else derivFamily fun (⟨x, _⟩ : Iio o) ↦ veblenWith f x
termination_by o
