compl_univ_iff

Mathlib.Order.BooleanAlgebra.Set

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

English

The complement of the universal set is the empty set, and conversely.

Русский

Дополнение вселенной равно пустому множеству, и обратно.

LaTeX

$$$s^{c} = \mathrm{univ} \iff s = \varnothing$$$

Lean4

@[simp]
theorem compl_univ_iff {s : Set α} : sᶜ = univ ↔ s = ∅ :=
  compl_eq_top

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

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

Разделы

Аффилиация

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