sUnion_union — Mathlib

English

Let S and T be collections of subsets of α. The union of the collections S ∪ T equals the union of the unions of S and of T: ⋃₀(S ∪ T) = ⋃₀S ∪ ⋃₀T.

Русский

Пусть S и T — коллекции подмножеств α. Объединение коллекций S ∪ T равно объединению объединений S и T: ⋃₀(S ∪ T) = ⋃₀S ∪ ⋃₀T.

LaTeX

$$$$ \\bigcup_{U \\in S \\cup T} U = \\Big( \\bigcup_{U \\in S} U \\Big) \\cup \\Big( \\bigcup_{U \\in T} U \\Big). $$$$

Lean4

theorem sUnion_union (S T : Set (Set α)) : ⋃₀ (S ∪ T) = ⋃₀ S ∪ ⋃₀ T :=
  sSup_union

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