compl_inter

Mathlib.Data.Finset.BooleanAlgebra

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

English

For Finsets s,t, the complement of the intersection equals the union of the complements: (s ∩ t)ᶜ = sᶜ ∪ tᶜ.

Русский

Для конечных множеств s,t выполняется: (s ∩ t)ᶜ = sᶜ ∪ tᶜ.

LaTeX

$$$ (s \\cap t)^{c} = s^{c} \\cup t^{c}$$$

Lean4

@[simp]
theorem compl_inter (s t : Finset α) : (s ∩ t)ᶜ = sᶜ ∪ tᶜ :=
  compl_inf

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

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

Разделы

Аффилиация

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