iUnion_ite — Mathlib

English

The indexed union of a pointwise ternary choice equals the union of corresponding indexed choices: iUnion i with ite(p(i)) yields union of those with p and not p.

Русский

Объединение по индексу ite равно объединению по частям: iUnionites.

LaTeX

$$$ \bigcup_i \mathrm{ite}(p(i), f(i), g(i)) = \bigcup_i \big( \mathrm{if } p(i) \text{ then } f(i) \text{ else } g(i) \big) = \bigcup_i (p(i) \Rightarrow f(i)) \cup \bigcup_i (\neg p(i) \Rightarrow g(i))$$$

Lean4

theorem iUnion_ite (f g : ι → Set α) :
    ⋃ i, (if p i then f i else g i) = (⋃ (i) (_ : p i), f i) ∪ ⋃ (i) (_ : ¬p i), g i :=
  iUnion_dite _ _ _

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