biUnion_insert — Mathlib

English

The union over x ∈ insert a s of t(x) equals t(a) union the union over x ∈ s of t(x).

Русский

Объединение по x ∈ insert(a,s) множества t(x) равно t(a) объединённому с объединением по x ∈ s t(x).

LaTeX

$$$\\\\bigcup_{x \\in insert(a, s)} t(x) = t(a) \\\\cup \\\\bigcup_{x \\in s} t(x)$$$

Lean4

theorem biUnion_insert (a : α) (s : Set α) (t : α → Set β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x := by simp

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