sUnion_eq_compl_sInter_compl — Mathlib

English

Let S be a collection of subsets of a set A. Then the union of all members of S equals the complement of the intersection of the complements of all members of S: for all A in S, A.

Русский

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

LaTeX

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

Lean4

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

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