iUnion_or — Mathlib

English

The union over ia of a family s ia equals the union over i and then a of s ⟨i,a⟩.

Русский

Объединение по индексации слагается как объединение по i, затем по a: ⋃ ia, s ia = ⋃ i, ⋃ a, s⟨i,a⟩.

LaTeX

$$$$\\bigcup_{ia} s_{ia} = \\bigcup_{i} \\bigcup_{a} s_{\\langle i,a\\rangle}$$$$

Lean4

theorem iUnion_or {p q : Prop} (s : p ∨ q → Set α) : ⋃ h, s h = (⋃ i, s (Or.inl i)) ∪ ⋃ j, s (Or.inr j) :=
  iSup_or

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