Commit 2026-05-25 09:15 8b24269d

feat: cofinal subset of regular cardinal is isomorphic to it (#38362) In set theory, one often identifies a cardinal c with its initial ordinal c.ord, and said ordinal with the lower set Iio c.ord. This is particularly pervasive in the theory of club and stationary subsets, where one often sees the hypothesis "let κ be a regular cardinal" in lieu of the more precise wording: that κ is an (infinite) well-order, whose order type equals the initial ordinal of its cardinality. We define a typeclass IsRegularCardinalOrder for this assumption. The benefit of using it is that our results won't apply only to Iio c.ord for regular c, but also to concrete types such as Nat, Cardinal, or Ordinal. As a proof of concept, we define Order.enum, a generalization of both Nat.nth and Ordinal.enumOrd. A future PR will deprecate the latter.