English
If the image of f over Ici a is not bounded above, the union of Ioc intervals covers the open end {f a}^+.
Русский
Если образ f по Ici a не ограничен сверху, объединение Ioc заполняет верхнюю окружность от f a.
LaTeX
$$\displaystyle \bigcup_{i \ge a} Ioc(f(i), f(\operatorname{succ} i)) = Ioi(f(a))$$
Lean4
theorem biUnion_Ici_Ioc_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} {a : α}
(hf : ∀ i ∈ Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Ici a)) : ⋃ i ∈ Ici a, Ioc (f i) (f (succ i)) = Ioi (f a) :=
by
apply subset_antisymm <| iUnion₂_subset fun i hi ↦ Ioc_subset_Ioc_left (hf i hi) |>.trans Ioc_subset_Ioi_self
intro b hb
contrapose! h2f
suffices ∀ i, a ≤ i → f i < b from ⟨b, by aesop (add simp [upperBounds, le_of_lt])⟩
exact Succ.rec (P := fun i _ ↦ f i < b) hb (by aesop)
