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 _ _ _