sdiff_insert_of_notMem

Mathlib.Data.Finset.SDiff

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

English

If a ≠ b and a ∉ s, then (insert a s) \ (insert b s) = { a }.

Русский

Если a ≠ b и a ∉ s, то (insert a s) \ (insert b s) = { a }.

LaTeX

$$$ a \neq b \land a \notin s \Rightarrow (insert(a,s) \setminus insert(b,s)) = \{a\} $$$

Lean4

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

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

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

Разделы

Аффилиация

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