Erasing an element from a finite set #
Main declarations #
Finset.erase
: For anya : α
,erase s a
returnss
with the elementa
removed.
Tags #
finite sets, finset
erase #
@[simp]
@[simp]
theorem
Finset.erase_eq_of_not_mem
{α : Type u_1}
[DecidableEq α]
{a : α}
{s : Finset α}
(h : a ∉ s)
:
@[simp]
@[simp]