insert_diff_singleton — Mathlib

English

For any set s and element a, inserting a into s \ {a} yields the same set as inserting a into s.

Русский

Для любого множества s и элемента a выполняется: вставка a в s \ {a} равна вставке a в s.

LaTeX

$$$$ \{a\} \cup (s \setminus \{a\}) = \{a\} \cup s. $$$$

Lean4

@[simp]
theorem insert_diff_singleton : insert a (s \ { a }) = insert a s := by
  simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]

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