Commit 2026-02-08 11:46 a022ca48

View on Github →

chore(SetTheory/Ordinal/Veblen): add recommended_spelling for epsilon and gamma functions (#34732) We also rename theorems from epsilon0 → epsilon_zero and gamma0 → gamma_zero, matching what we previously did with aleph1 → aleph_one in #33198.

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Veblen.lean

deleted theorem Ordinal.epsilon0_eq_nfp

deleted theorem Ordinal.epsilon0_le_of_omega0_opow_le

deleted theorem Ordinal.epsilon0_lt_gamma

added theorem Ordinal.epsilon_zero_eq_nfp

added theorem Ordinal.epsilon_zero_le_of_omega0_opow_le

added theorem Ordinal.epsilon_zero_lt_gamma

deleted theorem Ordinal.gamma0_eq_nfp

deleted theorem Ordinal.gamma0_le_of_veblen_le

added theorem Ordinal.gamma_zero_eq_nfp

added theorem Ordinal.gamma_zero_le_of_veblen_le

deleted theorem Ordinal.iterate_omega0_opow_lt_epsilon0

added theorem Ordinal.iterate_omega0_opow_lt_epsilon_zero

deleted theorem Ordinal.iterate_veblen_lt_gamma0

added theorem Ordinal.iterate_veblen_lt_gamma_zero

deleted theorem Ordinal.lt_epsilon0

added theorem Ordinal.lt_epsilon_zero

deleted theorem Ordinal.lt_gamma0

added theorem Ordinal.lt_gamma_zero