insert_compl_insert

Mathlib.Data.Finset.BooleanAlgebra

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

English

If a ∉ s, then insert a (insert a s)ᶜ = sᶜ.

Русский

Если a ∉ s, то insert a (insert a s)ᶜ = sᶜ.

LaTeX

$$$ a \\notin s \\Rightarrow \\mathrm{insert}\\ a\\ ((s \\cup \\{a\\})^{c}) = s^{c}$$$

Lean4

theorem insert_compl_insert (ha : a ∉ s) : insert a (insert a s)ᶜ = sᶜ := by
  simp_rw [compl_insert, insert_erase (mem_compl.2 ha)]

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

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

Разделы

Аффилиация

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