iUnion_Ico_right — Mathlib

English

Fix a. The union over all b of the half-open intervals [a, b) or [a, b] yields the ray [a, ∞). In particular, ⋃_{b} Ico(a,b) = Ici(a).

Русский

Зафиксируем левую границу a. Объединение по всем b полупервообразующих интервалов [a, b] даёт луч [a, ∞). То есть ⋃_{b} Ico(a,b) = [a, ∞).

LaTeX

$$$$\bigcup_{b} Ico(a,b) = Ici(a)$$$$

Lean4

@[simp]
theorem iUnion_Ico_right [NoMaxOrder α] (a : α) : ⋃ b, Ico a b = Ici a := by
  simp only [← Ici_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

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