iUnion_Ioo_coe_nat — Mathlib

English

Let a ∈ ENNReal. Then the union over all n ∈ ℕ of the open-intervals Ioo(a, n) equals the set of elements strictly greater than a, excluding the top element ∞; i.e. ⋃_{n∈ℕ} Ioo(a,n) = Ioi(a) \\ {∞}.

Русский

Пусть a ∈ ENNReal. Тогда объединение по n ∈ ℕ множеств Ioo(a, n) равно множеству x > a, за исключением верхнего элемента ∞; то есть ⋃_{n∈ℕ} Ioo(a,n) = Ioi(a) \\ {∞}.

LaTeX

$$$$\\bigcup_{n\\in\\mathbb{N}} Ioo(a,n) = Ioi(a) \\setminus \\{\\infty\\}$$$$

Lean4

@[simp]
theorem iUnion_Ioo_coe_nat : ⋃ n : ℕ, Ioo a n = Ioi a \ {∞} := by
  simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

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