biUnion_union — Mathlib

English

The union over x ∈ s ∪ t of u(x) equals the union over x ∈ s of u(x) plus the union over x ∈ t of u(x).

Русский

Объединение по x ∈ s ∪ t множества u(x) равно объединению по x ∈ s и по x ∈ t.

LaTeX

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

Lean4

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

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