iInter_Ici_coe_nat — Mathlib

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]

Похожие утверждения