iUnion_Icc_coe_nat — Mathlib

English

Let a ∈ ENNReal. Then the union over all n ∈ ℕ of the closed-intervals Icc(a, n) equals the interval Ici(a) with the top ∞ removed; formally, ⋃_{n∈ℕ} Icc(a,n) = Ici(a) \\ {∞}.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem iUnion_Icc_coe_nat : ⋃ n : ℕ, Icc a n = Ici a \ {∞} := by
  simp only [← Ici_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, diff_eq]

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