Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-27 23:26 a08d1797

View on Github →

refactor(set_theory/ordinal/*): ordinal.succ → order.succ (#14243) We inline the definition of ordinal.succ in the succ_order instance. This allows us to comfortably use all of the theorems about order.succ to our advantage.

Estimated changes

modified theorem cardinal.aleph'_succ
modified theorem cardinal.aleph_succ
modified theorem ordinal.blsub_const
modified theorem ordinal.blsub_le_bsup_succ
modified theorem ordinal.blsub_one
modified theorem ordinal.bsup_id_limit
modified def ordinal.lsub
modified theorem ordinal.lsub_const
modified theorem ordinal.lsub_unique
modified theorem ordinal.mul_add_one
modified theorem ordinal.mul_one_add
modified theorem ordinal.mul_succ
deleted theorem ordinal.succ_inj
deleted theorem ordinal.succ_le_succ
modified theorem ordinal.succ_lt_of_is_limit
modified theorem ordinal.succ_lt_of_not_succ
deleted theorem ordinal.succ_lt_succ
modified theorem ordinal.succ_one
modified theorem ordinal.succ_zero
modified theorem ordinal.sup_eq_lsub
modified theorem ordinal.sup_succ_eq_lsub
modified theorem ordinal.sup_succ_le_lsub
modified theorem ordinal.le_enum_succ
deleted theorem ordinal.lt_succ
deleted theorem ordinal.lt_succ_self
deleted def ordinal.succ
deleted theorem ordinal.succ_eq_add_one
deleted theorem ordinal.succ_le
deleted theorem ordinal.succ_ne_self