English
If a set s of ordinals is not bounded above, then the map a ↦ enumOrd(s, a) is strictly increasing: for all ordinals a and b, enumOrd(s, a) < enumOrd(s, b) if and only if a < b.
Русский
Если множество s ординалов не ограничено сверху, то отображение a ↦ enumOrd(s, a) является строгим вложением порядка: для любых ординалов a и b выполняется enumOrd(s, a) < enumOrd(s, b) тогда и только тогда, когда a < b.
LaTeX
$$$\forall s : \mathrm{Set}\ \mathrm{Ordinal},\, \neg \mathrm{BddAbove}(s) \Rightarrow \forall a,b : \mathrm{Ordinal},\, \mathrm{enumOrd}(s,a) < \mathrm{enumOrd}(s,b) \iff a < b$$$
Lean4
theorem enumOrd_lt_enumOrd (hs : ¬BddAbove s) {a b : Ordinal} : enumOrd s a < enumOrd s b ↔ a < b :=
(enumOrd_strictMono hs).lt_iff_lt
