English
For a set s not bounded above, the range of the enumeration function enumOrd(s) equals s.
Русский
Для множества s, не ограниченного сверху, образ функции enumOrd(s) равен самому s.
LaTeX
$$$\forall s : \mathrm{Set}\ \mathrm{Ordinal},\, \neg \mathrm{BddAbove}(s) \Rightarrow \mathrm{range}(\mathrm{enumOrd}(s)) = s$$$
Lean4
theorem range_enumOrd (hs : ¬BddAbove s) : range (enumOrd s) = s :=
by
ext a
let t := {b | a ≤ enumOrd s b}
constructor
· rintro ⟨b, rfl⟩
exact enumOrd_mem hs b
· intro ha
refine ⟨sInf t, (enumOrd_le_of_forall_lt ha ?_).antisymm ?_⟩
· intro b hb
by_contra! hb'
exact hb.not_ge (csInf_le' hb')
· exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩
