compl_sUnion — Mathlib

English

The complement of the union over a collection S equals the intersection of the complements of its members: (⋃₀ S)ᶜ = ⋂₀ (compl '' S).

Русский

Дополнение объединения над коллекцией S равно пересечению дополнений её элементов: (⋃₀ S)ᶜ = ⋂₀ (compl '' S).

LaTeX

$$$$ \\Big( \\bigcup_{U \\in S} U \\Big)^c = \\bigcap_{U \\in S} U^c. $$$$

Lean4

theorem compl_sUnion (S : Set (Set α)) : (⋃₀ S)ᶜ = ⋂₀ (compl '' S) :=
  ext fun x => by
    simp
      -- classical

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