# Erasing an element from a finite set #

## Main declarations #

- `Finset.erase`: For any `a : α`, `erase s a` returns `s` with the element `a` removed.

## Tags #

finite sets, finset

### erase #

source
def Finset.erase {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
Finset α

`erase s a` is the set `s - {a}`, that is, the elements of `s` which are not equal to `a`.

Equations

- s.erase a = { val := s.val.erase a, nodup := ⋯ }

Instances For

source
@[simp]
theorem Finset.erase_val {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :
(s.erase a).val = s.val.erase a
source
@[simp]
theorem Finset.mem_erase {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} :
a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s
source
theorem Finset.notMem_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
a ∉ s.erase a
source
@[deprecated Finset.notMem_erase (since := "2025-05-23")]
theorem Finset.not_mem_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
a ∉ s.erase a

Alias of `Finset.notMem_erase`.

source
theorem Finset.ne_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :
b ∈ s.erase a → b ≠ a
source
theorem Finset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :
b ∈ s.erase a → b ∈ s
source
theorem Finset.mem_erase_of_ne_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :
a ≠ b → a ∈ s → a ∈ s.erase b
source
theorem Finset.eq_of_mem_of_notMem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hs : b ∈ s) (hsa : b ∉ s.erase a) :
b = a

An element of `s` that is not an element of `erase s a` must be`a`.

source
@[deprecated Finset.eq_of_mem_of_notMem_erase (since := "2025-05-23")]
theorem Finset.eq_of_mem_of_not_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hs : b ∈ s) (hsa : b ∉ s.erase a) :
b = a

Alias of `Finset.eq_of_mem_of_notMem_erase`.

An element of `s` that is not an element of `erase s a` must be`a`.

source
@[simp]
theorem Finset.erase_eq_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) :
s.erase a = s
source
@[deprecated Finset.erase_eq_of_notMem (since := "2025-05-23")]
theorem Finset.erase_eq_of_not_mem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : a ∉ s) :
s.erase a = s

Alias of `Finset.erase_eq_of_notMem`.

source
@[simp]
theorem Finset.erase_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
s.erase a = s ↔ a ∉ s
source
theorem Finset.erase_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
s.erase a ≠ s ↔ a ∈ s
source
theorem Finset.erase_subset_erase {α : Type u_1} [DecidableEq α] (a : α) {s t : Finset α} (h : s ⊆ t) :
s.erase a ⊆ t.erase a
source
theorem Finset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
s.erase a ⊆ s
source
theorem Finset.subset_erase {α : Type u_1} [DecidableEq α] {a : α} {s t : Finset α} :
s ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s
source
@[simp]
theorem Finset.coe_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
↑(s.erase a) = ↑s \ {a}
source
theorem Finset.erase_idem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} :
(s.erase a).erase a = s.erase a
source
theorem Finset.erase_right_comm {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} :
(s.erase a).erase b = (s.erase b).erase a
source
theorem Finset.erase_inj {α : Type u_1} [DecidableEq α] {x y : α} (s : Finset α) (hx : x ∈ s) :
s.erase x = s.erase y ↔ x = y
source
theorem Finset.erase_injOn {α : Type u_1} [DecidableEq α] (s : Finset α) :
Set.InjOn s.erase ↑s