insert_sdiff_of_notMem

Mathlib.Data.Finset.SDiff

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

English

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

Русский

Если x не принадлежит t, то (insert x s) \ t = insert x (s \ t).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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