English
Let fastGrowingε₀ be the extension of the fast-growing hierarchy up to ε₀, defined by fastGrowingε₀(i) = fastGrowing( ((f)^{[i]})(0) ) with f(a) = a oadd 1 0. This uses the fundamental sequence converging to ε₀ given by ω, ω^ω, ω^(ω^ω), …
Русский
Пусть fastGrowingε₀ будет продолжением иерархии быстрого роста до ε₀, определённым как fastGrowingε₀(i) = fastGrowing( ((f)^{[i]})(0) ), где f(a) = a oadd 1 0. Это использует фундаментальную последовательность, сходящуюся к ε₀: ω, ω^ω, ω^(ω^ω), …
LaTeX
$$$$ \operatorname{fastGrowing}_{\varepsilon_0}(i) = \operatorname{fastGrowing}\big( ((a \mapsto a \mathrm{oadd} 1 0))^{[i]}(0) \big). $$$$
Lean4
/-- We can extend the fast growing hierarchy one more step to `ε₀` itself, using `ω ^ (ω ^ (⋯ ^ ω))`
as the fundamental sequence converging to `ε₀` (which is not an `ONote`). Extending the fast
growing hierarchy beyond this requires a definition of fundamental sequence for larger ordinals. -/
def fastGrowingε₀ (i : ℕ) : ℕ :=
fastGrowing ((fun a => a.oadd 1 0)^[i] 0) i
