doc-next-gen

Mathlib.Data.Finset.Erase

Module docstring

{"# 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 "}

Finset.erase definition
(s : Finset α) (a : α) : Finset α
Full source 
/-- `erase s a` is the set `s - {a}`, that is, the elements of `s` which are
  not equal to `a`. -/
def erase (s : Finset α) (a : α) : Finset α :=
  ⟨_, s.2.erase a⟩
Finite set element erasure
Informal description
For a finite set \( s \) over a type \( \alpha \) and an element \( a \in \alpha \), the operation \( \text{erase}(s, a) \) returns the finite set \( s \setminus \{a\} \), consisting of all elements of \( s \) that are not equal to \( a \).
Finset.erase_val theorem
(s : Finset α) (a : α) : (erase s a).1 = s.1.erase a
Full source 
@[simp]
theorem erase_val (s : Finset α) (a : α) : (erase s a).1 = s.1.erase a :=
  rfl
Underlying Multiset of Erased Finite Set Equals Erased Multiset
Informal description
For any finite set $s$ of elements of type $\alpha$ and any element $a \in \alpha$, the underlying multiset of $\operatorname{erase}(s, a)$ is equal to the multiset obtained by erasing one occurrence of $a$ from the underlying multiset of $s$. That is, $(\operatorname{erase}(s, a)).1 = s.1 \setminus \{a\}$.
Finset.mem_erase theorem
{a b : α} {s : Finset α} : a ∈ erase s b ↔ a ≠ b ∧ a ∈ s
Full source 
@[simp]
theorem mem_erase {a b : α} {s : Finset α} : a ∈ erase s ba ∈ erase s b ↔ a ≠ b ∧ a ∈ s :=
  s.2.mem_erase_iff
Membership in Finite Set Erasure: $a \in s \setminus \{b\} \leftrightarrow a \neq b \land a \in s$
Informal description
For any elements $a, b$ of a type $\alpha$ and any finite set $s$ of elements of $\alpha$, the element $a$ belongs to the set $s \setminus \{b\}$ if and only if $a \neq b$ and $a \in s$.
Finset.not_mem_erase theorem
(a : α) (s : Finset α) : a ∉ erase s a
Full source 
theorem not_mem_erase (a : α) (s : Finset α) : a ∉ erase s a :=
  s.2.not_mem_erase
Non-membership in Self-Erased Finite Set: $a \notin s \setminus \{a\}$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ of elements of $\alpha$, the element $a$ does not belong to the set obtained by removing $a$ from $s$, i.e., $a \notin s \setminus \{a\}$.
Finset.ne_of_mem_erase theorem
: b ∈ erase s a → b ≠ a
Full source 
theorem ne_of_mem_erase : b ∈ erase s a → b ≠ a := fun h => (mem_erase.1 h).1
Distinctness from Erased Element in Finite Set
Informal description
For any elements $a$ and $b$ of a type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $b$ belongs to the set $s \setminus \{a\}$, then $b \neq a$.
Finset.mem_of_mem_erase theorem
: b ∈ erase s a → b ∈ s
Full source 
theorem mem_of_mem_erase : b ∈ erase s a → b ∈ s :=
  Multiset.mem_of_mem_erase
Membership Preservation under Finite Set Erasure
Informal description
For any elements $a$ and $b$ of a type $\alpha$ and any finite set $s$ of elements of $\alpha$, if $b$ belongs to the set obtained by removing $a$ from $s$, then $b$ belongs to $s$.
Finset.mem_erase_of_ne_of_mem theorem
: a ≠ b → a ∈ s → a ∈ erase s b
Full source 
theorem mem_erase_of_ne_of_mem : a ≠ b → a ∈ s → a ∈ erase s b := by
  simp only [mem_erase]; exact And.intro
Membership Preservation under Erasure for Distinct Elements
Informal description
For any elements $a$ and $b$ in a type $\alpha$, if $a \neq b$ and $a$ belongs to a finite set $s$, then $a$ also belongs to the set obtained by erasing $b$ from $s$, i.e., $a \in \text{erase}(s, b)$.
Finset.erase_eq_of_not_mem theorem
{a : α} {s : Finset α} (h : a ∉ s) : erase s a = s
Full source 
@[simp]
theorem erase_eq_of_not_mem {a : α} {s : Finset α} (h : a ∉ s) : erase s a = s :=
  eq_of_veq <| erase_of_not_mem h
Erasure of Non-member Element Leaves Finite Set Unchanged
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ over $\alpha$, if $a$ does not belong to $s$, then erasing $a$ from $s$ leaves $s$ unchanged, i.e., $\text{erase}(s, a) = s$.
Finset.erase_ne_self theorem
: s.erase a ≠ s ↔ a ∈ s
Full source 
theorem erase_ne_self : s.erase a ≠ ss.erase a ≠ s ↔ a ∈ s :=
  erase_eq_self.not_left
Inequality of Set and Its Erasure $\leftrightarrow$ Membership
Informal description
For a finite set $s$ and an element $a$, the set obtained by removing $a$ from $s$ is not equal to $s$ if and only if $a$ is an element of $s$, i.e., $s \setminus \{a\} \neq s \leftrightarrow a \in s$.
Finset.erase_subset_erase theorem
(a : α) {s t : Finset α} (h : s ⊆ t) : erase s a ⊆ erase t a
Full source 
theorem erase_subset_erase (a : α) {s t : Finset α} (h : s ⊆ t) : eraseerase s a ⊆ erase t a :=
  val_le_iff.1 <| erase_le_erase _ <| val_le_iff.2 h
Subset Preservation under Element Erasure in Finite Sets
Informal description
For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ over $\alpha$, if $s$ is a subset of $t$, then the set obtained by removing $a$ from $s$ is a subset of the set obtained by removing $a$ from $t$, i.e., $s \setminus \{a\} \subseteq t \setminus \{a\}$.
Finset.erase_subset theorem
(a : α) (s : Finset α) : erase s a ⊆ s
Full source 
theorem erase_subset (a : α) (s : Finset α) : eraseerase s a ⊆ s :=
  Multiset.erase_subset _ _
Subset Property of Finite Set Erasure
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ over $\alpha$, the set obtained by removing $a$ from $s$ is a subset of $s$, i.e., $s \setminus \{a\} \subseteq s$.
Finset.subset_erase theorem
{a : α} {s t : Finset α} : s ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s
Full source 
theorem subset_erase {a : α} {s t : Finset α} : s ⊆ t.erase as ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s :=
  ⟨fun h => ⟨h.trans (erase_subset _ _), fun ha => not_mem_erase _ _ (h ha)⟩,
   fun h _b hb => mem_erase.2 ⟨ne_of_mem_of_not_mem hb h.2, h.1 hb⟩⟩
Subset Characterization via Element Erasure: $s \subseteq t \setminus \{a\} \leftrightarrow s \subseteq t \land a \notin s$
Informal description
For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ over $\alpha$, the set $s$ is a subset of $t \setminus \{a\}$ if and only if $s$ is a subset of $t$ and $a$ does not belong to $s$. In other words: $$ s \subseteq t \setminus \{a\} \leftrightarrow s \subseteq t \land a \notin s. $$
Finset.coe_erase theorem
(a : α) (s : Finset α) : ↑(erase s a) = (s \ { a } : Set α)
Full source 
@[simp, norm_cast]
theorem coe_erase (a : α) (s : Finset α) : ↑(erase s a) = (s \ {a} : Set α) :=
  Set.ext fun _ => mem_erase.trans <| by rw [and_comm, Set.mem_diff, Set.mem_singleton_iff, mem_coe]
Equality of Finite Set Erasure and Set Difference: $\text{erase}(s, a) = s \setminus \{a\}$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ over $\alpha$, the underlying set of the finite set obtained by erasing $a$ from $s$ is equal to the set difference $s \setminus \{a\}$. In symbols: $$ \text{erase}(s, a) = s \setminus \{a\}. $$
Finset.erase_idem theorem
{a : α} {s : Finset α} : erase (erase s a) a = erase s a
Full source 
theorem erase_idem {a : α} {s : Finset α} : erase (erase s a) a = erase s a := by simp
Idempotence of Finite Set Erasure: $\text{erase}(\text{erase}(s, a), a) = \text{erase}(s, a)$
Informal description
For any element $a$ of type $\alpha$ and any finite set $s$ over $\alpha$, erasing $a$ twice from $s$ is equivalent to erasing it once, i.e., $\text{erase}(\text{erase}(s, a), a) = \text{erase}(s, a)$.
Finset.erase_right_comm theorem
{a b : α} {s : Finset α} : erase (erase s a) b = erase (erase s b) a
Full source 
theorem erase_right_comm {a b : α} {s : Finset α} : erase (erase s a) b = erase (erase s b) a := by
  ext x
  simp only [mem_erase, ← and_assoc]
  rw [@and_comm (x ≠ a)]
Right Commutativity of Finite Set Erasure
Informal description
For any finite set $s$ over a type $\alpha$ and any two elements $a, b \in \alpha$, the operation of erasing $a$ and then $b$ from $s$ is equal to the operation of erasing $b$ and then $a$ from $s$. That is, $\text{erase}(\text{erase}(s, a), b) = \text{erase}(\text{erase}(s, b), a)$.
Finset.erase_inj theorem
{x y : α} (s : Finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y
Full source 
theorem erase_inj {x y : α} (s : Finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y := by
  refine ⟨fun h => eq_of_mem_of_not_mem_erase hx ?_, congr_arg _⟩
  rw [← h]
  simp
Injectivity of Finite Set Erasure: $s \setminus \{x\} = s \setminus \{y\} \leftrightarrow x = y$
Informal description
For any finite set $s$ over a type $\alpha$ and elements $x, y \in \alpha$ such that $x \in s$, the equality $s \setminus \{x\} = s \setminus \{y\}$ holds if and only if $x = y$.
Finset.erase_injOn theorem
(s : Finset α) : Set.InjOn s.erase s
Full source 
theorem erase_injOn (s : Finset α) : Set.InjOn s.erase s := fun _ _ _ _ => (erase_inj s ‹_›).mp
Injectivity of Finite Set Erasure on Its Own Elements
Informal description
For any finite set $s$ over a type $\alpha$, the erasure function $\text{erase}(s, \cdot)$ is injective on $s$. That is, for any $x, y \in s$, if $\text{erase}(s, x) = \text{erase}(s, y)$, then $x = y$.