Theorems · Definition · logic and foundations

ONote.fastGrowing

ONote → ℕ → ℕ

The fast growing hierarchy for ordinal notations < ε₀. This is a sequence of functions ℕ → ℕ indexed by ordinals, with the definition: * f_0(n) = n + 1 * f_(α + 1)(n) = f_α^[n](n) * f_α(n) = f_(α[n])(n) where α is a limit ordinal and α[i] is the fundamental sequence converging to α

Defined in

Mathlib.SetTheory.Ordinal.Notation

Cited by

10 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound