compl_sInter — Mathlib

English

Let S be a collection of subsets of A. Then the complement of the intersection of all sets in S equals the union of their complements: (⋂_{A∈S} A)^c = ⋃_{A∈S} A^c.

Русский

Пусть S — множество подмножеств α. Тогда дополнение пересечения всех элементов S равно объединению их дополнений: (⋂_{A∈S} A)^c = ⋃_{A∈S} A^c.

LaTeX

$$$$ \\left( \\bigcap_{A \\in S} A \\right)^c = \\bigcup_{A \\in S} A^c. $$$$

Lean4

theorem compl_sInter (S : Set (Set α)) : (⋂₀ S)ᶜ = ⋃₀ (compl '' S) := by
  rw [sUnion_eq_compl_sInter_compl, compl_compl_image]
    -- classical

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