compl_union_self

Mathlib.Order.BooleanAlgebra.Set

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

English

The union of a set’s complement with the set equals the universal set.

Русский

Объединение дополнения множества с самим множеством равно вселенному множеству.

LaTeX

$$$s^{c} \cup s = \mathrm{univ}$$$

Lean4

@[simp]
theorem compl_union_self (s : Set α) : sᶜ ∪ s = univ := by rw [union_comm, union_compl_self]

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

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

Разделы

Аффилиация

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