insert_sdiff_self_of_mem

Mathlib.Data.Finset.SDiff

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

English

If a ∈ s, then insert a (s \ {a}) = s.

Русский

Если a ∈ s, то добавление a в (s \ {a}) восстанавливает s.

LaTeX

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

Lean4

@[simp]
theorem insert_sdiff_self_of_mem (ha : a ∈ s) : insert a (s \ { a }) = s := by grind

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

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

Разделы

Аффилиация

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