sdiff_insert

Mathlib.Data.Finset.Basic

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

English

Let S, T be finite subsets of a set A and x an element of A. Then S \\ (T ∪ {x}) = (S \\ T) \\ {x}.

Русский

Пусть S, T — конечные подмножества множества A и элемент x ∈ A. Тогда S \ (T ∪ {x}) = (S \\ T) \\ {x}.

LaTeX

$$$S \\setminus (T \\cup \\{x\\}) = (S \\setminus T) \\setminus \\{x\\}$$$

Lean4

theorem sdiff_insert (s t : Finset α) (x : α) : s \ insert x t = (s \ t).erase x := by grind

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

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

Разделы

Аффилиация

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