Documentation

Mathlib.Data.Finset.Erase

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 #

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

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

@[simp]

theorem Finset.erase_val {α : Type u_1} [DecidableEq α] (s : Finset α) (a : α) :

(s.erase a).val = s.val.erase a

@[simp]

theorem Finset.mem_erase {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} :

a ∈ s.erase b ↔ a ≠ b ∧ a ∈ s

theorem Finset.notMem_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :

¬a ∈ s.erase a

theorem Finset.ne_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :

b ∈ s.erase a → b ≠ a

theorem Finset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :

b ∈ s.erase a → b ∈ s

theorem Finset.mem_erase_of_ne_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :

a ≠ b → a ∈ s → a ∈ s.erase b

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.

@[simp]

theorem Finset.erase_eq_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : ¬a ∈ s) :

s.erase a = s

@[simp]

theorem Finset.erase_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :

s.erase a = s ↔ ¬a ∈ s

theorem Finset.erase_ne_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :

s.erase a ≠ s ↔ a ∈ s

theorem Finset.erase_subset_erase {α : Type u_1} [DecidableEq α] (a : α) {s t : Finset α} (h : s ⊆ t) :

s.erase a ⊆ t.erase a

theorem Finset.erase_subset {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :

s.erase a ⊆ s

theorem Finset.subset_erase {α : Type u_1} [DecidableEq α] {a : α} {s t : Finset α} :

s ⊆ t.erase a ↔ s ⊆ t ∧ ¬a ∈ s

@[simp]

theorem Finset.coe_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :

↑(s.erase a) = ↑s \ {a}

theorem Finset.erase_idem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} :

(s.erase a).erase a = s.erase a

theorem Finset.erase_right_comm {α : Type u_1} [DecidableEq α] {a b : α} {s : Finset α} :

(s.erase a).erase b = (s.erase b).erase a

theorem Finset.erase_inj {α : Type u_1} [DecidableEq α] {x y : α} (s : Finset α) (hx : x ∈ s) :

s.erase x = s.erase y ↔ x = y

theorem Finset.erase_injOn {α : Type u_1} [DecidableEq α] (s : Finset α) :

Set.InjOn s.erase ↑s