Commit 2025-10-01 11:17 78e78cba

View on Github →

chore: remove deprecated declarations in SetTheory.Ordinal.Family (#30102) All the FIXME There is undeprecated material below still depending on this?! lemmas, with lemma names changed and (non-problematic) deprecations added as necessary.

Estimated changes

modified theorem Ordinal.IsNormal.bsup
deleted theorem Ordinal.IsNormal.sup
added theorem Ordinal.bsup'_eq_iSup
added theorem Ordinal.bsup_eq_iSup
deleted theorem Ordinal.bsup_eq_sup'
deleted theorem Ordinal.bsup_eq_sup
added theorem Ordinal.iSup'_eq_bsup
modified theorem Ordinal.iSup_eq_bsup
added theorem Ordinal.iSup_eq_iSup
added theorem Ordinal.iSup_eq_lsub
added theorem Ordinal.iSup_le_lsub
deleted theorem Ordinal.le_sup
modified def Ordinal.lsub
modified theorem Ordinal.lsub_eq_zero_iff
modified theorem Ordinal.lsub_le_iff
deleted theorem Ordinal.lsub_le_sup_succ
modified theorem Ordinal.lsub_notMem_range
modified theorem Ordinal.lsub_pos
modified theorem Ordinal.lt_lsub_iff
deleted theorem Ordinal.ne_sup_iff_lt_sup
modified theorem Ordinal.sSup_eq_bsup
deleted def Ordinal.sup
deleted theorem Ordinal.sup_const
deleted theorem Ordinal.sup_eq_bsup'
deleted theorem Ordinal.sup_eq_bsup
deleted theorem Ordinal.sup_eq_lsub
deleted theorem Ordinal.sup_eq_sup
deleted theorem Ordinal.sup_le
deleted theorem Ordinal.sup_le_iff
deleted theorem Ordinal.sup_le_lsub
deleted theorem Ordinal.sup_succ_eq_lsub
deleted theorem Ordinal.sup_succ_le_lsub
deleted theorem Ordinal.sup_sum
deleted theorem Ordinal.sup_typein_limit
deleted theorem Ordinal.sup_typein_succ
deleted theorem Ordinal.sup_unique