union_eq_compl_compl_inter_compl

Mathlib.Order.BooleanAlgebra.Set

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

English

The union of two sets equals the complement of the intersection of their complements.

Русский

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

LaTeX

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

Lean4

theorem union_eq_compl_compl_inter_compl (s t : Set α) : s ∪ t = (sᶜ ∩ tᶜ)ᶜ :=
  ext fun _ => or_iff_not_and_not

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

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

Разделы

Аффилиация

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