iInter_eq_compl_iUnion_compl — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInter_eq_compl_iUnion_compl (s : ι → Set β) : ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ := by
  simp only [compl_iUnion, compl_compl]

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