English
A well-ordered set is order-isomorphic to the set of ordinals smaller than its type; the function enum r maps the o-th element to the corresponding element in α.
Русский
Хорошо упорядоченное множество изоморфно множеству ординалов, меньших по типу; функция enum r сопоставляет o-й элемент соответствующему элементу в α.
LaTeX
$$$\\text{enum}(r) : (\\cdot < \\cdot : Iio(\\mathrm{type} r) \\to Iio(\\mathrm{type} r) ) \\cong_r r$$$
Lean4
/-- A well order `r` is order-isomorphic to the set of ordinals smaller than `type r`.
`enum r ⟨o, h⟩` is the `o`-th element of `α` ordered by `r`.
That is, `enum` maps an initial segment of the ordinals, those less than the order type of `r`, to
the elements of `α`. -/
@[simps! symm_apply_coe]
def enum (r : α → α → Prop) [IsWellOrder α r] : (· < · : Iio (type r) → Iio (type r) → Prop) ≃r r :=
(typein r).subrelIso
