sInter_union_sInter — Mathlib

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

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