set_biUnion_insert_update — Mathlib

English

If x is not in t, the union over insert x t of updates of f at x by s equals s union the union over t of f.

Русский

Если x не принадлежит t, то объединение по insert x t от обновления f в x до s равно $s \\cup \\bigcup_{i\\in t} f(i)$.

LaTeX

$$$$ \\bigcup_{i \\in \\operatorname{insert} x t} \\mathrm{update}(f, x, s)(i) = s \\cup \\bigcup_{i \\in t} f(i) $$$$

Lean4

theorem set_biUnion_insert_update {x : α} {t : Finset α} (f : α → Set β) {s : Set β} (hx : x ∉ t) :
    ⋃ i ∈ insert x t, @update _ _ _ f x s i = s ∪ ⋃ i ∈ t, f i :=
  iSup_insert_update f hx

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