insert_diff_insert — Mathlib

English

For any a and set s, inserting a into s \ {a} t? remains equal to inserting a into (s \ t): insert a (s \ insert a t) = insert a (s \ t).

Русский

Для любых a и множества s верно: insert a (s \ insert a t) = insert a (s \ t).

LaTeX

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

Lean4

@[simp]
theorem insert_diff_insert : insert a (s \ insert a t) = insert a (s \ t) := by
  rw [← union_singleton (s := t), ← diff_diff, insert_diff_singleton]

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