erase_insert_eq_erase

Mathlib.Data.Finset.Basic

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

English

Inserting a into a Finset and then erasing a yields the same Finset as erasing a directly.

Русский

Добавление a в Finset затем удаление a даёт тот же Finset, что и прямое удаление a.

LaTeX

$$$\\operatorname{erase}(\\operatorname{insert} a\\ s)\\, a = \\operatorname{erase} a\\ s$$$

Lean4

@[simp]
theorem erase_insert_eq_erase (s : Finset α) (a : α) : (insert a s).erase a = s.erase a := by grind

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

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

Разделы

Аффилиация

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