insert_compl_self

Mathlib.Data.Finset.BooleanAlgebra

URI: https://scilib.ai/kg/mathlib#Finset.insert_compl_self

English

The complement of a singleton {a} equals univ with a removed: {a}ᶜ = univ \\\\ {a}.

Русский

Дополнение множества {a} равно универсума удалённому элементу a: {a}ᶜ = univ \\\\ {a}.

LaTeX

$$$ {a}^{c} = univ \\setminus \\{a\\}$$$

Lean4

@[simp]
theorem insert_compl_self (x : α) : insert x ({ x }ᶜ : Finset α) = univ := by
  rw [← compl_erase, erase_singleton, compl_empty]

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

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

Разделы

Аффилиация

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