English
Let (s_i) be a family of subsets of α indexed by i ∈ I, and let t be a family of subsets of β indexed by elements of α. Then the intersection over x in the union of all s_i of t(x) equals the intersection over i of the intersection over x in s_i of t(x).
Русский
Пусть (s_i) — семейство подмножеств α, индексируемое i ∈ I, и пусть t: α → Set β задаёт подмножества β в зависимости от x ∈ α. Тогда ⋂_{x ∈ ⋃_i s_i} t(x) = ⋂_i ⋂_{x ∈ s_i} t(x).
LaTeX
$$$$ \bigcap_{x \in \bigcup_{i} s_i} t(x) = \bigcap_{i} \bigcap_{x \in s_i} t(x) $$$$
Lean4
theorem biInter_iUnion (s : ι → Set α) (t : α → Set β) : ⋂ x ∈ ⋃ i, s i, t x = ⋂ (i) (x ∈ s i), t x := by
simp [@iInter_comm _ ι]
