Commit 2025-02-13 03:54 48361102

View on Github →

feat(SetTheory/Ordinal/Veblen): the two-arguments Veblen function (#18611) We define the Veblen function veblen o a on ordinals, so that veblen 0 a = ω ^ a and veblen o enumerates the common fixed points of veblen o' for o' < o. We then prove some basic properties.

Estimated changes

added theorem Ordinal.cmp_veblen
added theorem Ordinal.cmp_veblenWith
added theorem Ordinal.left_le_veblen
added def Ordinal.veblen
added theorem Ordinal.veblenWith_inj
added theorem Ordinal.veblenWith_pos
added theorem Ordinal.veblen_inj
added theorem Ordinal.veblen_pos
added theorem Ordinal.veblen_succ
added theorem Ordinal.veblen_zero