English
If the well-order type of α is at most the supremum of the types of f i, then the range of f is unbounded in α.
Русский
Пусть (α, r) — хорошо упорядоченный тип. Если тип r не превосходит верхнюю границу по i равно sup_i typein r(f i), то множество range(f) не ограничено сверху в α.
LaTeX
$$$$ \\text{If } \\mathrm{IsWellOrder}(\\alpha, r) \\text{ and } h: \\operatorname{type}(r) \\le \\big\\lvert\\operatorname{range}(f)\\big\\rvert_{?}, \\text{ then } \\operatorname{Unbounded}_r(\\operatorname{range}(f)). $$$$
Lean4
theorem unbounded_range_of_le_iSup {α β : Type u} (r : α → α → Prop) [IsWellOrder α r] (f : β → α)
(h : type r ≤ ⨆ i, typein r (f i)) : Unbounded r (range f) :=
(not_bounded_iff _).1 fun ⟨x, hx⟩ =>
h.not_gt <|
lt_of_le_of_lt (Ordinal.iSup_le fun y => ((typein_lt_typein r).2 <| hx _ <| mem_range_self y).le)
(typein_lt_type r x)
