Commit 2025-05-08 13:37 f77d2271

View on Github →

feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals (#17802) We define the epsilon function ε_ o = veblen 1 o, and the gamma function Γ_ o which enumerates the fixed points of veblen · 0.

Estimated changes

added theorem Ordinal.iterate_lt_nfp
added theorem Ordinal.epsilon_pos
added theorem Ordinal.gamma0_eq_nfp
added def Ordinal.gamma
added theorem Ordinal.gamma_inj
added theorem Ordinal.gamma_le_gamma
added theorem Ordinal.gamma_lt_gamma
added theorem Ordinal.gamma_pos
added theorem Ordinal.isNormal_gamma
added theorem Ordinal.lt_epsilon0
added theorem Ordinal.lt_gamma0
added theorem Ordinal.monotone_gamma
modified theorem Ordinal.veblenWith_succ
modified theorem Ordinal.veblen_succ