sInter_union — Mathlib

English

Let S and T be collections of subsets of α. The intersection over S ∪ T equals the intersection over S intersected with the intersection over T: ⋂₀(S ∪ T) = ⋂₀S ∩ ⋂₀T.

Русский

Пусть S и T — коллекции подмножеств α. Пересечение над S ∪ T равно пересечению S и T: ⋂₀(S ∪ T) = ⋂₀S ∩ ⋂₀T.

LaTeX

$$$$ \\bigcap_{U \\in S \\cup T} U = \\Big( \\bigcap_{U \\in S} U \\Big) \\cap \\Big( \\bigcap_{U \\in T} U \\Big). $$$$

Lean4

theorem sInter_union (S T : Set (Set α)) : ⋂₀ (S ∪ T) = ⋂₀ S ∩ ⋂₀ T :=
  sInf_union

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