Small initial segments

Stream: maths

[Violeta Hernández]

I've recently come to realize that there are two different ways to assign a rank function to a well-founded order. The obvious one would be docs#well_founded.rank, which returns an ordinal in the same universe as the original type. But in some important cases, including ordinals (trivially), cardinals, ZFC sets and combinatorial games, one is in fact able to assign ordinals in a universe one lower.

[Violeta Hernández]

The necessary condition is that for α : Type (u+1), all initial segments (meaning intervals Iio a) are small.{u}.

[Violeta Hernández]

I was thinking about implementing this as a typeclass. As arguments, it would have the canonical (transitive) well-founded relation on the type, and a proof that all initial segments are small.

[Violeta Hernández]

@Yuyang Zhao @Junyan Xu what do you think about this?

[Junyan Xu]

Sounds good to me! I don't think we have (<) or Iio defined on ZFC sets and games though.

[Yuyang Zhao]

I used docs#subrel for this in #18527 recently.

[Violeta Hernández]

It's probably best to take in an arbitrary relation for this typeclass. The subsequence relation on games should definitely not be using the < symbol.