erase_right_comm — Mathlib

English

Let s be a finite set and a,b be elements. Removing a from s and then removing b yields the same result as removing b first and then removing a.

Русский

Пусть s — конечное множество, и элементы a,b. Удаление a из s и затем удаление b соответствует удалению b из s и затем удалению a.

LaTeX

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

Lean4

theorem erase_right_comm {a b : α} {s : Finset α} : erase (erase s a) b = erase (erase s b) a := by grind

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