iInter_dite — Mathlib

English

For predicate p on i and families f,g, the intersection of a conditional sets equals the intersection of the two groupings: iInter dite identity.

Русский

Для предиката p на i и семейств f,g пересечение условных множеств равно пересечению двух групп: iInter dite.

LaTeX

$$$ \bigcap_i (\text{if } p(i) \text{ then } f(i) \text{ else } g(i)) = \bigcap_i (p(i) \Rightarrow f(i)) \cap \bigcap_i (\neg p(i) \Rightarrow g(i)) $$$

Lean4

theorem iInter_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 :=
  iInf_dite _ _ _

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