Commit 2026-10-17 11:31 953b504c

View on Github →

feat(SetTheory/Ordinal): classify exponential principal ordinals (#43633) Complete TODO: Prove that the exponential principal ordinals are `0`, `1`, `2`, `ω`, or `ε_ x` in Mathlib/SetTheory/Ordinal/Principal.lean By the way, the original TODO was wrong because 1 is not an exponential principal ordinal (it requires $0^0=1<1$ which is false).

Estimated changes

Modified Mathlib/SetTheory/Ordinal/Principal.lean

added theorem Ordinal.IsPrincipal.mul_of_opow

added theorem Ordinal.isPrincipal_opow_iff_omega0_opow_eq_self

added theorem Ordinal.isPrincipal_opow_iff_zero_or_two_or_omega0_or_omega0_opow_eq

added theorem Ordinal.isPrincipal_opow_two

added theorem Ordinal.isSuccLimit_of_isPrincipal_opow

added theorem Ordinal.omega0_lt_and_isPrincipal_opow_iff

added theorem Ordinal.omega0_lt_of_omega0_opow_eq_self

Modified Mathlib/SetTheory/Ordinal/Veblen.lean

added theorem Ordinal.isPrincipal_opow_epsilon

added theorem Ordinal.isPrincipal_opow_iff_zero_or_two_or_omega0_or_epsilon

added theorem Ordinal.mem_range_epsilon