mathlib3

4e7e5a6e - feat(set_theory/ordinal_arithmetic): Enumerating unbounded sets of ordinals with ordinals (#10979)

feat(set_theory/ordinal_arithmetic): Enumerating unbounded sets of ordinals with ordinals (#10979) This PR introduces `enum_ord`, which enumerates an unbounded set of ordinals using ordinals. This is used to build an explicit order isomorphism `enum_ord.order_iso`.