insert_sdiff_of_mem

Mathlib.Data.Finset.SDiff

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

English

If x ∈ t, then (insert x s) \ t = s \ t.

Русский

Если x ∈ t, то (insert x s) \ t = s \ t.

LaTeX

$$$ x \in t \Rightarrow \operatorname{insert}(x,s) \setminus t = s \setminus t $$$

Lean4

theorem insert_sdiff_of_mem (s : Finset α) {x : α} (h : x ∈ t) : insert x s \ t = s \ t := by grind

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

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

Разделы

Аффилиация

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