erase_sdiff_comm — Mathlib

English

Removing a from a set then taking the set difference with another equals taking the set difference first and then removing a.

Русский

Удаление a из множества затем вычитание другого множества эквивалентно сначала вычитанию, затем удалению a.

LaTeX

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

Lean4

theorem erase_sdiff_comm (s t : Finset α) (a : α) : s.erase a \ t = (s \ t).erase a := by grind

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