Commit 2025-04-03 11:14 b0081eeb

feat: generalize normal functions (#20504) In ordinal/cardinal arithmetic, a normal function is a strictly monotonic continuous function. We opt for an equivalent definition that's more lightweight and often more convenient: a normal function is a strictly monotonic function where, for a successor limit a, the value f a is the LUB of f b for b < a. The predicate Ordinal.IsNormal already exists. This generalization serves two purposes:

1. We can now talk about normality of functions between ordinals and cardinals, rather than functions that are strictly between ordinals. Examples include Cardinal.ord, Cardinal.aleph, and Cardinal.beth.
2. This is also useful to my project on formalizing ordinal notations, as I can now state that addition, multiplication, etc. defined on an ordinal notation are also normal functions. A future PR will deprecate Ordinal.IsNormal in favor of this new predicate.