English
Let f and g be two-argument families of subsets. Then the union of intersections equals the intersection over all four-indexed unions: (⋂_{i1,i2} f_{i1,i2}) ∪ (⋂_{j1,j2} g_{j1,j2}) = ⋂_{i1,i2,j1,j2} (f_{i1,i2} ∪ g_{j1,j2}).
Русский
Пусть f и g — пары индексов для подмножеств; объединение пересечений равно пересечению по всем объединениям.
LaTeX
$$$\left(\bigcap_{i_1,i_2} f_{i_1,i_2}\right) \cup \bigcap_{j_1,j_2} g_{j_1,j_2} = \bigcap_{i_1,i_2,j_1,j_2} \bigl( f_{i_1,i_2} \cup g_{j_1,j_2} \bigr)$$$
Lean4
theorem iInter₂_union_iInter₂ {ι₁ κ₁ : 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 [iInter_union, union_iInter]
