compl_insert

Mathlib.Data.Finset.BooleanAlgebra

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

English

The complement of inserting a into s equals the complement of s with a erased: (insert a s)ᶜ = sᶜ.erase a.

Русский

Дополнение вставки a в s равно удалению a из дополнения s: (insert a s)ᶜ = sᶜ.erase a.

LaTeX

$$$ (s \\cup \\{a\\})^{c} = s^{c} \\setminus \\{a\\}$$$

Lean4

@[simp]
theorem compl_insert : (insert a s)ᶜ = sᶜ.erase a := by
  ext
  simp only [not_or, mem_insert, mem_compl, mem_erase]

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

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

Разделы

Аффилиация

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