compl_iUnion

Mathlib.Data.Set.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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