English
Let s : α ⊕ β → Set γ. Then the union over all elements of the sum is the union of the two separate unions over α and β: ⋃ x, s x = (⋃ x, s (Sum.inl x)) ∪ (⋃ x, s (Sum.inr x)).
Русский
Пусть s : α ⊕ β → Set γ. Тогда объединение по всем элементам суммы равно объединению по частям: ⋃ x, s x = (⋃ x, s (Sum.inl x)) ∪ (⋃ x, s (Sum.inr x)).
LaTeX
$$$$\\bigcup_{x} s(x) = \\bigl(\\bigcup_{x} s(\\mathrm{Sum.inl}\\, x)\\bigr) \\cup \\bigl(\\bigcup_{x} s(\\mathrm{Sum.inr}\\, x)\\bigr).$$$$
Lean4
theorem iUnion_sum {s : α ⊕ β → Set γ} : ⋃ x, s x = (⋃ x, s (.inl x)) ∪ ⋃ x, s (.inr x) :=
iSup_sum