Commit 2024-09-16 17:23 1410abf9

refactor(SetTheory/Ordinal/Arithmetic): Ditch Ordinal.sup (#15820) Ordinal.sup is just iSup with more restricted universes. This is the first part in a series of refactors aimed at putting the ordinal API in line with the API of other lattices. Theorems like le_iSup were kept as protected theorems within the Ordinal namespace, as they can be useful when you do know that the input type lives in a smaller universe. That said, using them indiscriminately will make the universes in theorems stricter than they need to be. I kept sup within the API for bsup, lsub, blsub, and mex, as I plan to refactor those individually in the near future.