Documentation

Mathlib.Data.Finset.Erase

Erasing an element from a finite set #

Main declarations #

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
    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 α) :
      as.erase a
      @[deprecated Finset.notMem_erase (since := "2025-05-23")]
      theorem Finset.not_mem_erase {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) :
      as.erase a

      Alias of Finset.notMem_erase.

      theorem Finset.ne_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :
      b s.erase ab a
      theorem Finset.mem_of_mem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :
      b s.erase ab s
      theorem Finset.mem_erase_of_ne_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} :
      a ba sa s.erase b
      theorem Finset.eq_of_mem_of_notMem_erase {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hs : b s) (hsa : bs.erase a) :
      b = a

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

      @[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 : bs.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 bea.

      @[simp]
      theorem Finset.erase_eq_of_notMem {α : Type u_1} [DecidableEq α] {a : α} {s : Finset α} (h : as) :
      s.erase a = s
      @[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 : as) :
      s.erase a = s

      Alias of Finset.erase_eq_of_notMem.

      @[simp]
      theorem Finset.erase_eq_self {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :
      s.erase a = s as
      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 as
      @[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 α) :