mathlib

9f818ce0 - feat(set_theory/ordinal_basic): `o.out.α` is equivalent to the ordinals below `o` (#13876)