erase_sdiff_erase — Mathlib

English

For any Finset s and element a, erase s a is equal to s \\\\ {a}.

Русский

Для любого Finset s и элемента a, erase s a равно s \\\\ {a}.

LaTeX

$$$ \\forall (s : Finset \\alpha) (a : \\alpha), erase s a = s \\\\{ a \\}$$$

Lean4

theorem erase_sdiff_erase (hab : a ≠ b) (hb : b ∈ s) : s.erase a \ s.erase b = { b } := by ext;
  aesop
    -- TODO: Do we want to delete this lemma and `Finset.disjUnion_singleton`,
    -- or instead add `Finset.union_singleton`/`Finset.singleton_union`?

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