set_biUnion_union — Mathlib

English

Union over x in s ∪ t of u(x) equals union over x in s of u(x) together with union over x in t of u(x).

Русский

Объединение по индексу из s ∪ t равно объединению по s и объединению по t, объединённому вместе.

LaTeX

$$$$ \\bigcup_{x \\in s \\cup t} u(x) = \\left(\\bigcup_{x \\in s} u(x)\\right) \\cup \\left(\\bigcup_{x \\in t} u(x)\\right) $$$$

Lean4

theorem set_biUnion_union (s t : Finset α) (u : α → Set β) : ⋃ x ∈ s ∪ t, u x = (⋃ x ∈ s, u x) ∪ ⋃ x ∈ t, u x :=
  iSup_union

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