Ordinals as a ω-complete partial order

Stream: maths

[Violeta Hernández]

PR #15578 made me realize we might have some duplicated API between the theory of fixed points of ordinal functions, and the fixed points in a ω-complete partial order.

[Violeta Hernández]

For instance, docs#OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint has a version on ordinals as docs#Ordinal.nfp. It's not exactly the same since nfp works on an arbitrary function, but its API does show that it is a fixed point when the argument is a normal function (which in particular is a order hom with x ≤ f x.

[Violeta Hernández]

I'm not sure to what degree we can restate results in terms of ω-CPOs. For instance, I wouldn't expect docs#Ordinal.nfpFamily, which takes the next fixed point of any small family of functions, to generalize. That being said, there's probably better ways to state this. A TODO remark states that this just generalizes the statement that an intersection of club sets is a club set (which @Nir Paz has been working on getting onto Mathlib).

[Violeta Hernández]

Something else I'm not expecting to generalize: the derivative docs#Ordinal.deriv of a normal function. The fact that you can enumerate an unbounded set of the ordinals by themselves is something very specific to them, as it requires an inaccessible cardinality.

[Violeta Hernández]

(It'd be nice to redefine deriv as the docs#Ordinal.enumOrd of the fixed points. The enumOrd API is currently a bit ugly, but I'm working on cleaning it up.)

[Violeta Hernández]

So, what's the course of action? I'm thinking Ordinal.nfp can be turned into something like IsNormal.iterateChain, but I'm not sure what to do with Ordinal.nfpFamily or everything else.

[Violeta Hernández]

Important context: my original reason for adding these functions was to define the https://en.wikipedia.org/wiki/Veblen_function. This is an ordinal-indexed sequence where each function enumerates the common fixed points of all the previous ones.

[Violeta Hernández]

So, if we can otherwise state that the fixed points of a small family of normal functions are unbounded, we might be able to do without nfpFamily.