iUnion_sum — Mathlib

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

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