iUnion_insert_eq_range_union_iUnion

English

For any x(i) and t(i), the union over i of insert(x(i), t(i)) equals the union of the range of x and the union over i of t(i): ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i.

Русский

Для последовательности x(i) и t(i) объединение по i вставок x(i) в t(i) равно объединению образа x и объединению ⋃ i t(i).

LaTeX

$$$$ \\bigcup_{i} \\operatorname{insert}(x(i), t(i)) = \\operatorname{range} x \\cup \\bigcup_{i} t(i). $$$$

Lean4

theorem iUnion_insert_eq_range_union_iUnion {ι : Type*} (x : ι → β) (t : ι → Set β) :
    ⋃ i, insert (x i) (t i) = range x ∪ ⋃ i, t i := by
  simp_rw [← union_singleton, iUnion_union_distrib, union_comm, iUnion_singleton_eq_range]

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