English
Let f and g be two-argument families of subsets. Then the intersection of the unions equals the union of all intersections: ⋃_{i1,i2} f_{i1,i2} ∩ ⋃_{j1,j2} g_{j1,j2} = ⋃_{i1,i2,j1,j2} (f_{i1,i2} ∩ g_{j1,j2}).
Русский
Пусть f и g — пары индексов для подмножеств; пересечение объединений равно объединению всех пересечений.
LaTeX
$$$\bigcup_{i_1,i_2} f_{i_1,i_2} \cap \bigcup_{j_1,j_2} g_{j_1,j_2} = \bigcup_{i_1,i_2,j_1,j_2} \bigl( f_{i_1,i_2} \cap g_{j_1,j_2} \bigr)$$$
Lean4
theorem iUnion₂_inter_iUnion₂ {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*} (f : ∀ i₁, ι₂ i₁ → Set α)
(g : ∀ j₁, k₂ j₁ → Set α) :
(⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂ := by
simp_rw [iUnion_inter, inter_iUnion]
