sInter_diff_singleton_univ — Mathlib

English

For any collection s of subsets of α, the intersection over s minus the universal set equals the intersection over s: ⋂₀ (s \\ { univ }) = ⋂₀ s.

Русский

Для любой коллекции s подмножеств α пересечение над s без универсума равно пересечению над s: ⋂₀ (s \\ { univ }) = ⋂₀ s.

LaTeX

$$$$ \\bigcap_{U \\in s \\setminus \\{ \\text{univ} \\}} U = \\bigcap_{U \\in s} U. $$$$

Lean4

@[simp]
theorem sInter_diff_singleton_univ (s : Set (Set α)) : ⋂₀ (s \ { univ }) = ⋂₀ s :=
  sInf_diff_singleton_top s

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