compl_singleton_eq

Mathlib.Order.BooleanAlgebra.Set

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

English

The complement of a singleton equals the set of all elements not equal to the singleton element.

Русский

Дополнение единичного множества есть множество элементов, не равных данному элементу.

LaTeX

$$$\{ a \}^{c} = \{x \mid x \neq a\}$$$

Lean4

theorem compl_singleton_eq (a : α) : { a }ᶜ = {x | x ≠ a} :=
  rfl

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

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

Разделы

Аффилиация

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