iUnion_eq_compl_iInter_compl — Mathlib

English

The union over i of s_i equals the complement of the intersection over i of the complements: ⋃ i s_i = (⋂ i (s_i^c))^c.

Русский

Объединение по i равно дополнению пересечения по i дополнений: ⋃ i s_i = (⋂ i s_i^c)^c.

LaTeX

$$$$ \\bigcup_{i} s_i = \\left( \\bigcap_{i} s_i^c \\right)^c $$$$

Lean4

theorem iUnion_eq_compl_iInter_compl (s : ι → Set β) : ⋃ i, s i = (⋂ i, (s i)ᶜ)ᶜ := by
  simp only [compl_iInter, compl_compl]
    -- classical -- complete_boolean_algebra

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