basic): Order isomorphism between `o.out.α` and `set.Iio o` (#14074)

Commit

3 years ago

feat(set_theory/ordinal/basic): Order isomorphism between `o.out.α` and `set.Iio o` (#14074) This strengthens the previously existing equivalence.

Author

vihdzp

Parents