iUnion_Icc_left — Mathlib

English

Let α be a preorder. For every b in α, the union over all a of the closed interval [a, b] is the set of all elements not exceeding b; i.e., ⋃_a [a, b] = {x ∈ α | x ≤ b}.

Русский

Пусть α — упорядоченное множество с предопорядком. Для произвольного b выполняется объединение по всем a не более чем [a, b] даёт множество элементов, не превосходящих b; т.е. ⋃_a [a, b] = {x | x ≤ b}.

LaTeX

$$$$\bigcup_a Icc(a,b) = Iic(b)$$$$

Lean4

@[simp]
theorem iUnion_Icc_left (b : α) : ⋃ a, Icc a b = Iic b := by
  simp only [← Ici_inter_Iic, ← iUnion_inter, iUnion_Ici, univ_inter]

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