compl_iInter

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.compl_iInter

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem compl_iInter (s : ι → Set β) : (⋂ i, s i)ᶜ = ⋃ i, (s i)ᶜ :=
  compl_iInf

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru