English
Under suitable hypotheses, the union over i ≥ a of intervals [f(i), f(succ i)) equals [f(a), ∞).
Русский
При подходящих гипотезах объединение по i ≥ a интервалов [f(i), f(succ i)) равно [f(a), ∞).
LaTeX
$$\displaystyle \bigcup_{i \ge a} [f(i), f(\operatorname{succ}i)) = [f(a), \infty)$$
Lean4
theorem biUnion_Ici_Ico_map_succ [SuccOrder α] [IsSuccArchimedean α] [LinearOrder β] {f : α → β} {a : α}
(hf : ∀ i ∈ Ici a, f a ≤ f i) (h2f : ¬BddAbove (f '' Ici a)) : ⋃ i ∈ Ici a, Ico (f i) (f (succ i)) = Ici (f a) :=
by
apply subset_antisymm <| iUnion₂_subset fun i hi ↦ Ico_subset_Ico_left (hf i hi) |>.trans Ico_subset_Ici_self
intro b hb
contrapose! h2f
use b
simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
exact Succ.rec (P := fun i _ ↦ f i ≤ b) hb (by aesop)
