iUnion_Ico_coe_nat — Mathlib

English

Let a ∈ ENNReal. Then the union over n ∈ ℕ of the half-open intervals Ico(a, n) equals Ici(a) with the top removed; i.e. ⋃_{n∈ℕ} Ico(a,n) = Ici(a) \\ {∞}.

Русский

Пусть a ∈ ENNReal. Тогда объединение по n ∈ ℕ множеств Ico(a, n) равно Ici(a) без ∞; то есть ⋃_{n∈ℕ} Ico(a,n) = Ici(a) \\ {∞}.

LaTeX

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

Lean4

@[simp]
theorem iUnion_Ico_coe_nat : ⋃ n : ℕ, Ico a n = Ici a \ {∞} := by
  simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio_coe_nat, diff_eq]

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