Theorems · Definition · logic and foundations

Ordinal.veblenWith

(Ordinal.{u} → Ordinal.{u}) → Ordinal.{u} → Ordinal.{u} → Ordinal.{u}

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.

Defined in

Mathlib.SetTheory.Ordinal.Veblen

Cited by

34 results in Mathlib

Foundations

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