insert_iUnion — Mathlib

English

For any element x and a family t_i of sets, the insertion of x into the union of all t_i equals the union over i of the insertions into t_i: insert x (⋃_i t_i) = ⋃_i insert x (t_i).

Русский

Для любого элемента x и семейства множеств t_i верно: вставка x в объединение всех t_i равна объединению по i вставок x в t_i: insert x (⋃_i t_i) = ⋃_i insert x (t_i).

LaTeX

$$$ \operatorname{insert}(x, \bigcup_i t_i) = \bigcup_i \operatorname{insert}(x, t_i) $$$$

Lean4

theorem insert_iUnion [Nonempty ι] (x : β) (t : ι → Set β) : insert x (⋃ i, t i) = ⋃ i, insert x (t i) := by
  simp_rw [← union_singleton, iUnion_union]
    -- classical

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