insert_diff_singleton_comm — Mathlib

English

If a ≠ b, then inserting a into s \ {b} equals inserting a into s then removing b: insert a (s \ {b}) = insert a s \ {b}.

Русский

Пусть a ≠ b. Тогда вставка a в s \ {b} равна вставке a в s, затем удалению b: insert a (s \ {b}) = insert a s \ {b}.

LaTeX

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

Lean4

theorem insert_diff_singleton_comm (hab : a ≠ b) (s : Set α) : insert a (s \ { b }) = insert a s \ { b } := by
  simp_rw [← union_singleton, union_diff_distrib, diff_singleton_eq_self (mem_singleton_iff.not.2 hab.symm)]

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