English
Let S and T be sets of subsets of α. Then the intersection of the unions equals the intersection over all pairs p ∈ S × T of p.1 ∪ p.2.
Русский
Пусть S и T — множества подмножеств α. Тогда пересечение объединений равно пересечению по всем парам p ∈ S × T от p.1 ∪ p.2.
LaTeX
$$$$ \\bigcap S.\\bigcup T = \\bigcap_{p \\in S \\times T} (p.1 \\cup p.2). $$$$
Lean4
theorem sInter_union_sInter {S T : Set (Set α)} : ⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, (p : Set α × Set α).1 ∪ p.2 :=
sInf_sup_sInf