set_biUnion_insert — Mathlib

English

When a single element a is inserted into a finite set s, the union over the new set equals the union over {a} together with the union over the old set.

Русский

При вставке элемента a в конечное множество s объединение над новым множеством равно объединению над {a} и объединением над старым множеством.

LaTeX

$$$$ \\bigcup_{x \\in \\operatorname{insert} a s} u(x) = u(a) \\cup \\bigcup_{x \\in s} u(x) $$$$

Lean4

theorem set_biUnion_insert (a : α) (s : Finset α) (t : α → Set β) : ⋃ x ∈ insert a s, t x = t a ∪ ⋃ x ∈ s, t x :=
  iSup_insert a s t

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