Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 09:29 31e60c87

View on Github →

feat(set_theory/{ordinal, ordinal_arithmetic}): Add various instances for o.out.α (#12508)

Estimated changes

Modified src/measure_theory/card_measurable_space.lean

Modified src/set_theory/cardinal_ordinal.lean

Modified src/set_theory/ordinal.lean

added theorem ordinal.enum_le_enum'

added theorem ordinal.enum_zero_eq_bot

added theorem ordinal.enum_zero_le'

added theorem ordinal.enum_zero_le

added theorem ordinal.le_enum_succ

added theorem ordinal.lt_succ

added def ordinal.out_order_bot_of_pos

added theorem ordinal.typein_le_typein'

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.enum_succ_eq_top

deleted theorem ordinal.has_succ_of_is_limit

added theorem ordinal.has_succ_of_type_succ_lt

deleted theorem ordinal.lt_succ

added theorem ordinal.out_no_max_of_succ_lt