English
Let a,b ∈ ENNReal. The intersection over n ∈ ℕ of the half-closed interval Ici(n) is the singleton {∞}; that is, ⋂_{n∈ℕ} Ici(n) = {∞}.
Русский
Пусть a,b ∈ ENNReal. Пересечение по n ∈ ℕ множеств Ici(n) равно единичному множеству {∞}; то есть ⋂_{n∈ℕ} Ici(n) = {∞}.
LaTeX
$$$$\\bigcap_{n\\in\\mathbb{N}} Ici(n) = \\{\\infty\\}$$$$
Lean4
@[simp]
theorem iInter_Ici_coe_nat : ⋂ n : ℕ, Ici (n : ℝ≥0∞) = {∞} := by
simp only [← compl_Iio, ← compl_iUnion, iUnion_Iio_coe_nat, compl_compl]