Commit 2024-10-08 09:15 f681278e

chore(SetTheory/Ordinal/Arithmetic): deprecate Ordinal.mex and Ordinal.bmex (#16989) There isn't any reason not to use sInf sᶜ instead - both nimber arithmetic and Grundy values work perfectly without mex. The one nontrivial result was that the mex of an indexed family is less than the successor of the cardinal of the indexing type - this has been reproved as sInf_compl_lt_ord_succ and sInf_compl_lt_ord_succ_lift.