English
Let a ∈ ENNReal. Then the union over all n ∈ ℕ of the closed-intervals Icc(a, n) equals the interval Ici(a) with the top ∞ removed; formally, ⋃_{n∈ℕ} Icc(a,n) = Ici(a) \\ {∞}.
Русский
Пусть a ∈ ENNReal. Тогда объединение по n ∈ ℕ множеств Icc(a, n) равно интервалу Ici(a) с удалением ∞; то есть ⋃_{n∈ℕ} Icc(a,n) = Ici(a) \\ {∞}.
LaTeX
$$$$\\bigcup_{n\\in\\mathbb{N}} Icc(a,n) = Ici(a) \\setminus \\{\\infty\\}$$$$
Lean4
@[simp]
theorem iUnion_Icc_coe_nat : ⋃ n : ℕ, Icc a n = Ici a \ {∞} := by
simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]