Commit 2024-10-09 05:25 27e1331f

refactor(SetTheory/Ordinal/Enum): better definition for Ordinal.enumOrd (#16962) The old definition was a hassle to work with, to the extent we first had to prove its equivalence to the current definition. This can be sidestepped thanks to the termination checker. This also has the benefit of avoiding Ordinal.blsub, which I'm planning to deprecate in the near future. There's some lemmas that have to be outright removed rather than deprecated (since it'd be difficult to reprove them), but hopefully all of them have a clear case for being internal workings that should have been private to begin with. Other improvements:

• We move all of this to its own file, since it's not really needed within Ordinal/Arithmetic.
• We also replace Set.Unbounded (· < ·) with the more canonical ¬ BddAbove throughout.