iInter_Ioi_coe_nat — Mathlib

English

Let a,b ∈ ENNReal. The intersection over n ∈ ℕ of the open-interval Ioi(n) is {∞}; i.e. ⋂_{n∈ℕ} Ioi(n) = {∞}.

Русский

Пусть a,b ∈ ENNReal. Пересечение по n ∈ ℕ множеств Ioi(n) равно {∞}; то есть ⋂_{n∈ℕ} Ioi(n) = {∞}.

LaTeX

$$$$\\bigcap_{n\\in\\mathbb{N}} Ioi(n) = \\{\\infty\\}$$$$

Lean4

@[simp]
theorem iInter_Ioi_coe_nat : ⋂ n : ℕ, Ioi (n : ℝ≥0∞) = {∞} := by
  simp only [← compl_Iic, ← compl_iUnion, iUnion_Iic_coe_nat, compl_compl]

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