iInter_inter_distrib — Mathlib

English

The intersection over i of s_i ∩ t_i equals the intersection of the intersections: ⋂ i (s_i ∩ t_i) = (⋂ i s_i) ∩ (⋂ i t_i).

Русский

Пересечение по i распределяется между пересечениями: ⋂ i (s_i ∩ t_i) = (⋂ i s_i) ∩ (⋂ i t_i).

LaTeX

$$$$ \\bigcap_{i} (s_i \\cap t_i) = \\left( \\bigcap_{i} s_i \\right) \\cap \\left( \\bigcap_{i} t_i \\right) $$$$

Lean4

theorem iInter_inter_distrib (s : ι → Set β) (t : ι → Set β) : ⋂ i, s i ∩ t i = (⋂ i, s i) ∩ ⋂ i, t i :=
  iInf_inf_eq

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