Commit 2023-02-22 19:59 ccd53ee6

View on Github →

feat: port SetTheory.Ordinal.Principal (#2442)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Ordinal/Principal.lean

added theorem Ordinal.Principal.iterate_lt

added def Ordinal.Principal

added theorem Ordinal.add_absorp

added theorem Ordinal.add_omega

added theorem Ordinal.add_omega_opow

added def Ordinal.blsub₂

added theorem Ordinal.exists_lt_add_of_not_principal_add

added theorem Ordinal.lt_blsub₂

added theorem Ordinal.mul_eq_opow_log_succ

added theorem Ordinal.mul_lt_omega_opow

added theorem Ordinal.mul_omega

added theorem Ordinal.mul_omega_dvd

added theorem Ordinal.mul_omega_opow_opow

added theorem Ordinal.mul_principal_add_is_principal_add

added theorem Ordinal.nfp_le_of_principal

added theorem Ordinal.op_eq_self_of_principal

added theorem Ordinal.opow_omega

added theorem Ordinal.opow_principal_add_of_principal_add

added theorem Ordinal.principal_add_iff_add_left_eq_self

added theorem Ordinal.principal_add_iff_add_lt_ne_self

added theorem Ordinal.principal_add_iff_zero_or_omega_opow

added theorem Ordinal.principal_add_isLimit

added theorem Ordinal.principal_add_of_le_one

added theorem Ordinal.principal_add_of_principal_mul

added theorem Ordinal.principal_add_of_principal_mul_opow

added theorem Ordinal.principal_add_omega

added theorem Ordinal.principal_add_omega_opow

added theorem Ordinal.principal_add_one

added theorem Ordinal.principal_iff_principal_swap

added theorem Ordinal.principal_mul_iff_le_two_or_omega_opow_opow

added theorem Ordinal.principal_mul_iff_mul_left_eq

added theorem Ordinal.principal_mul_isLimit

added theorem Ordinal.principal_mul_of_le_two

added theorem Ordinal.principal_mul_omega

added theorem Ordinal.principal_mul_omega_opow_opow

added theorem Ordinal.principal_mul_one

added theorem Ordinal.principal_mul_two

added theorem Ordinal.principal_nfp_blsub₂

added theorem Ordinal.principal_one_iff

added theorem Ordinal.principal_opow_omega

added theorem Ordinal.principal_zero

added theorem Ordinal.unbounded_principal