insert_sdiff_insert'

Mathlib.Data.Finset.SDiff

URI: https://scilib.ai/kg/mathlib#Finset.insert_sdiff_insert'

English

If x ∉ s, then s \ insert x t = s \ t for all t.

Русский

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

LaTeX

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

Lean4

theorem insert_sdiff_insert' (hab : a ≠ b) (ha : a ∉ s) : insert a s \ insert b s = { a } := by ext; aesop

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

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

Разделы

Аффилиация

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