Commit 2025-03-21 01:28 d27a8090

View on Github →

chore: remove >6 month old deprecations in SetTheory (#23164) This covers statements from 2024-09-01 to 2024-09-21 inclusive. The removed statements have quite a few set_option linter.deprecated trues among them.

Estimated changes

deleted theorem Ordering.orElse_eq_lt
deleted theorem Ordering.swap_orElse
deleted theorem Fin.orderEmbedding_eq
deleted theorem Fin.strictMono_unique
deleted theorem Cardinal.isLimit_aleph0
deleted theorem Cardinal.IsLimit.succ_lt
deleted def Cardinal.IsLimit
deleted theorem Ordinal.IsNormal.self_le
deleted theorem Ordinal.mk_initialSeg
deleted theorem Ordinal.CNF_fst_le
deleted theorem Ordinal.enumOrd_def
deleted def Ordinal.bmex
deleted theorem Ordinal.bmex_le_blsub
deleted theorem Ordinal.bmex_le_of_ne
deleted theorem Ordinal.bmex_monotone
deleted theorem Ordinal.exists_of_lt_bmex
deleted theorem Ordinal.exists_of_lt_mex
deleted theorem Ordinal.le_bmex_of_forall
deleted theorem Ordinal.le_mex_of_forall
deleted def Ordinal.mex
deleted theorem Ordinal.mex_le_lsub
deleted theorem Ordinal.mex_le_of_ne
deleted theorem Ordinal.mex_monotone
deleted theorem Ordinal.mex_not_mem_range
deleted theorem Ordinal.ne_bmex
deleted theorem Ordinal.ne_mex
deleted theorem WellFounded.rank_eq
deleted def PSet.Arity.Equiv
deleted theorem PSet.Arity.equiv_const
deleted def PSet.Definable.EqMk
deleted def PSet.Definable.Resp
deleted theorem PSet.Definable.eq
deleted def PSet.Resp.Equiv
deleted def PSet.Resp.eval
deleted def PSet.Resp.evalAux
deleted theorem PSet.Resp.eval_val
deleted def PSet.Resp.f
deleted def PSet.Resp
deleted theorem ZFSet.eval_mk