Commit 2022-05-13 05:13 7b7af48b
View on Github →feat(set_theory/ordinal/basic): Order isomorphism between o.out.α and set.Iio o (#14074)
This strengthens the previously existing equivalence.
feat(set_theory/ordinal/basic): Order isomorphism between o.out.α and set.Iio o (#14074)
This strengthens the previously existing equivalence.