offDiag_univ

Mathlib.Data.Set.Prod

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

English

The off-diagonal of the universal set equals the complement of the diagonal.

Русский

Вне диагонали универсума совпадает с дополнением диагонали.

LaTeX

$$$ (\mathrm{univ} : Set \alpha).offDiag = (\operatorname{diagonal} \alpha)^{c} $$$

Lean4

@[simp]
theorem offDiag_univ : (univ : Set α).offDiag = (diagonal α)ᶜ :=
  ext <| by simp

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

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

Разделы

Аффилиация

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