insert_diff_eq_singleton

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.insert_diff_eq_singleton

English

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

Русский

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

LaTeX

$$$\bigl(a \notin s\bigr) \Rightarrow \left( (\operatorname{insert}(a,s) \setminus s) = \{a\} \right)$$$

Lean4

@[simp]
theorem insert_diff_eq_singleton {a : α} {s : Set α} (h : a ∉ s) : insert a s \ s = { a } := by grind

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

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

Разделы

Аффилиация

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