erase_insert_subset — Mathlib

English

For any a and finite s, removing a from the set obtained by inserting a into s yields a subset of s.

Русский

Для любого a и конечного множества s удаление элемента a из множества, полученного добавлением a к s, является подмножеством s.

LaTeX

$$$ (insert\\ a\\ s) \\setminus\\{a\\} \\subseteq s$$$

Lean4

theorem erase_insert_subset (a : α) (s : Finset α) : erase (insert a s) a ⊆ s :=
  subset_insert_iff.1 <| Subset.rfl

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