compls_union

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.compls_union

English

Complement distributes over union: (s ∪ t)ᶜˢ = sᶜˢ ∪ tᶜˢ.

Русский

Комплемент распределяется по объединению: (s ∪ t)ᶜˢ = sᶜˢ ∪ tᶜˢ.

LaTeX

$$$(s\cup t)^{\!c_s} = s^{\!c_s} \cup t^{\!c_s}$$$

Lean4

@[simp]
theorem compls_union (s t : Finset α) : (s ∪ t)ᶜˢ = sᶜˢ ∪ tᶜˢ :=
  map_union _ _

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

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

Разделы

Аффилиация

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