iUnion_Ioo_right — Mathlib

English

For any a, the union over b of the open intervals (a,b) is (a, ∞). That is, ⋃_{b} Ioo(a,b) = Ioi(a).

Русский

Для фиксированного a объединение по всем b открытых интервалов (a,b) равно (a, ∞). То есть ⋃_{b} Ioo(a,b) = Ioi(a).

LaTeX

$$$$\bigcup_{b} Ioo(a,b) = Ioi(a)$$$$

Lean4

@[simp]
theorem iUnion_Ioo_right [NoMaxOrder α] (a : α) : ⋃ b, Ioo a b = Ioi a := by
  simp only [← Ioi_inter_Iio, ← inter_iUnion, iUnion_Iio, inter_univ]

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