Commit 2024-12-12 20:12 2e4e286e

feat(SetTheory/Ordinal/Basic): recursion on well-orders (#19678) To define an ordinal-valued function, it suffices to define its values on well-ordered types. This will be used to redefine the cofinality of an ordinal as the cofinality of a well-order with its order type.