iUnion_Ico_left — Mathlib

English

Let α be a preorder. For every b, the union over a of the half-open intervals [a, b) equals the open-closed interval (-∞, b); i.e., ⋃_a [a, b) = {x | x < b}.

Русский

Пусть α — упорядоченное множество с предопорядком. Для произвольного b объединение по всем a полуинтервалов [a, b) даёт весь интервал (-∞, b); т.е. ⋃_a [a, b) = {x | x < b}.

LaTeX

$$$$\bigcup_a Ico(a,b) = Iio(b)$$$$

Lean4

@[simp]
theorem iUnion_Ico_left (b : α) : ⋃ a, Ico a b = Iio b := by
  simp only [← Ici_inter_Iio, ← iUnion_inter, iUnion_Ici, univ_inter]

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