iUnion_dite — Mathlib

English

For predicates p on index i, and decompositions f,g, the union over i of a conditional set equals the union of the corresponding branches: iUnion dite identity.

Русский

Для предиката p на индексе i и разложений f,g равенство объединения по условию iUnion dite.

LaTeX

$$$ \bigcup_i \left( \text{if } p(i) \text{ then } f(i) \text{ else } g(i) \right) = \bigcup_i (\text{if } p(i) \text{ then } f(i) \text{ else } g(i)) $$$

Lean4

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

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