sInter_eq_compl_sUnion_compl — Mathlib

English

For any S ⊆ P(A), the intersection of all sets in S equals the complement of the union of their complements: ⋂_{A∈S} A = (⋃_{A∈S} A^c)^c.

Русский

Для любого S ⊆ P(A) пересечение всех элементов S равно дополнению к объединению дополнений элементов S: ⋂_{A∈S} A = (⋃_{A∈S} A^c)^c.

LaTeX

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

Lean4

theorem sInter_eq_compl_sUnion_compl (S : Set (Set α)) : ⋂₀ S = (⋃₀ (compl '' S))ᶜ := by
  rw [← compl_compl (⋂₀ S), compl_sInter]

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