iInter_ite — Mathlib

English

For predicate p on i, iInter of ite yields a decomposition into intersections over p_i and not p_i branches.

Русский

Для предиката p на i iInter of ite разлагает на пересечения ветвей p_i и ¬p_i.

LaTeX

$$$ \bigcap_i \mathrm{ite}(p(i), f(i), g(i)) = \bigcap_i (p(i) \Rightarrow f(i)) \cap \bigcap_i (\neg p(i) \Rightarrow g(i)) $$$

Lean4

theorem iInter_ite (f g : ι → Set α) :
    ⋂ i, (if p i then f i else g i) = (⋂ (i) (_ : p i), f i) ∩ ⋂ (i) (_ : ¬p i), g i :=
  iInter_dite _ _ _

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