insert_sdiff_cancel

Mathlib.Data.Finset.SDiff

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

English

If a ∉ s, then insert a s \ s = {a}.

Русский

Если a не в s, то вставка a в s разность с s равна {a}.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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