erase_ssubset_insert — Mathlib

English

Erasing the single element from a singleton set yields the empty set.

Русский

Удаление единственного элемента из множества-одиночки даёт пустое множество.

LaTeX

$$$$ ({a})\text{ erase } a = \emptyset. $$$$

Lean4

theorem erase_ssubset_insert (s : Finset α) (a : α) : s.erase a ⊂ insert a s :=
  ssubset_iff_exists_subset_erase.2 <| by exact ⟨a, mem_insert_self _ _, by grw [← subset_insert]⟩

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