Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-01 10:02 ca2a99dd

View on Github →

feat(set_theory/ordinal_arithmetic): Normal functions evaluated at ω (#11687)

Estimated changes

Modified src/set_theory/ordinal.lean

added theorem ordinal.eq_zero_or_pos

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.is_normal.apply_omega

added theorem ordinal.sup_add_nat

added theorem ordinal.sup_mul_nat

added theorem ordinal.sup_nat_cast

added theorem ordinal.sup_opow_nat