compl_ne_eq_singleton

Mathlib.Order.BooleanAlgebra.Set

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

English

Let α be a type and a ∈ α. Then the complement of the set { x ∈ α : x ≠ a } is { a }.

Русский

Пусть α — множество (тип) и a ∈ α. Тогда дополнение множества { x ∈ α : x ≠ a } равно { a }.

LaTeX

$$$\{x \in \alpha \mid x \ne a\}^{c} = \{a\}$$$

Lean4

@[simp]
theorem compl_ne_eq_singleton (a : α) : {x | x ≠ a}ᶜ = { a } :=
  compl_compl _

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

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

Разделы

Аффилиация

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