compl_prod_eq_union

Mathlib.Data.Set.Prod

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

English

The complement of s × t equals (sᶜ × univ) ∪ (univ × tᶜ).

Русский

Дополнение к s × t равно (sᶜ × univ) ∪ (univ × tᶜ).

LaTeX

$$$ (s \times t)^{c} = (s^{c} \times \mathrm{univ}) \cup (\mathrm{univ} \times t^{c}) $$$

Lean4

theorem compl_prod_eq_union {α β : Type*} (s : Set α) (t : Set β) : (s ×ˢ t)ᶜ = (sᶜ ×ˢ univ) ∪ (univ ×ˢ tᶜ) := by grind

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

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

Разделы

Аффилиация

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