doc-next-gen

Mathlib.Data.Finset.SDiff

Module docstring

{"# Difference of finite sets

Main declarations

  • Finset.instSDiff: Defines the set difference s \\ t for finsets s and t.
  • Finset.instGeneralizedBooleanAlgebra: Finsets almost have a boolean algebra structure

Tags

finite sets, finset

","### sdiff "}

Finset.sdiff_val theorem
(s₁ s₂ : Finset α) : (s₁ \ s₂).val = s₁.val - s₂.val
Full source 
@[simp]
theorem sdiff_val (s₁ s₂ : Finset α) : (s₁ \ s₂).val = s₁.val - s₂.val :=
  rfl
Multiset Representation of Set Difference for Finite Sets
Informal description
For any two finite sets $s_1$ and $s_2$ of type $\alpha$, the underlying multiset of their set difference $s_1 \setminus s_2$ is equal to the subtraction of the underlying multiset of $s_2$ from the underlying multiset of $s_1$. That is, $\text{val}(s_1 \setminus s_2) = \text{val}(s_1) - \text{val}(s_2)$, where $\text{val}$ denotes the underlying multiset representation.
Finset.mem_sdiff theorem
: a ∈ s \ t ↔ a ∈ s ∧ a ∉ t
Full source 
@[simp]
theorem mem_sdiff : a ∈ s \ ta ∈ s \ t ↔ a ∈ s ∧ a ∉ t :=
  mem_sub_of_nodup s.2
Membership in Set Difference of Finite Sets: $a \in s \setminus t \leftrightarrow (a \in s) \land (a \notin t)$
Informal description
For any element $a$ of type $\alpha$ and any finite sets $s$ and $t$ of $\alpha$, the element $a$ belongs to the set difference $s \setminus t$ if and only if $a$ belongs to $s$ and $a$ does not belong to $t$. That is, \[ a \in s \setminus t \leftrightarrow (a \in s) \land (a \notin t). \]
Finset.inter_sdiff_self theorem
(s₁ s₂ : Finset α) : s₁ ∩ (s₂ \ s₁) = ∅
Full source 
@[simp]
theorem inter_sdiff_self (s₁ s₂ : Finset α) : s₁ ∩ (s₂ \ s₁) = ∅ :=
  eq_empty_of_forall_not_mem <| by
    simp only [mem_inter, mem_sdiff]; rintro x ⟨h, _, hn⟩; exact hn h
Intersection with Set Difference is Empty
Informal description
For any two finite sets $s_1$ and $s_2$ of type $\alpha$, the intersection of $s_1$ with the set difference $s_2 \setminus s_1$ is the empty set, i.e., $s_1 \cap (s_2 \setminus s_1) = \emptyset$.
Finset.instGeneralizedBooleanAlgebra instance
: GeneralizedBooleanAlgebra (Finset α)
Full source 
instance : GeneralizedBooleanAlgebra (Finset α) :=
  { sup_inf_sdiff := fun x y => by
      simp only [Finset.ext_iff, mem_union, mem_sdiff, inf_eq_inter, sup_eq_union, mem_inter,
        ← and_or_left, em, and_true, implies_true]
    inf_inf_sdiff := fun x y => by
      simp only [Finset.ext_iff, inter_sdiff_self, inter_empty, inter_assoc, false_iff,
        inf_eq_inter, not_mem_empty, bot_eq_empty, not_false_iff, implies_true] }
Generalized Boolean Algebra Structure on Finite Sets
Informal description
For any type $\alpha$, the collection of finite subsets of $\alpha$ forms a generalized Boolean algebra, where the lattice operations are given by intersection and union, the bottom element is the empty set, and the relative complement operation is given by set difference.
Finset.not_mem_sdiff_of_not_mem_left theorem
(h : a ∉ s) : a ∉ s \ t
Full source 
theorem not_mem_sdiff_of_not_mem_left (h : a ∉ s) : a ∉ s \ t := by simp [h]
Non-membership in Set Difference from Non-membership in First Set
Informal description
For any element $a$ and finite sets $s$ and $t$ of type $\alpha$, if $a$ is not an element of $s$, then $a$ is not an element of the set difference $s \setminus t$.
Finset.union_sdiff_of_subset theorem
(h : s ⊆ t) : s ∪ t \ s = t
Full source 
theorem union_sdiff_of_subset (h : s ⊆ t) : s ∪ t \ s = t :=
  sup_sdiff_cancel_right h
Union with Difference Equals Superset for Finite Sets
Informal description
For any finite sets $s$ and $t$ of type $\alpha$, if $s$ is a subset of $t$, then the union of $s$ with the set difference $t \setminus s$ equals $t$, i.e., $s \cup (t \setminus s) = t$.
Finset.sdiff_union_of_subset theorem
{s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₂ \ s₁ ∪ s₁ = s₂
Full source 
theorem sdiff_union_of_subset {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₂ \ s₁s₂ \ s₁ ∪ s₁ = s₂ :=
  (union_comm _ _).trans (union_sdiff_of_subset h)
Union of Set Difference with Subset Equals Superset for Finite Sets
Informal description
For any finite sets $s_1$ and $s_2$ of type $\alpha$, if $s_1$ is a subset of $s_2$, then the union of the set difference $s_2 \setminus s_1$ with $s_1$ equals $s_2$, i.e., $(s_2 \setminus s_1) \cup s_1 = s_2$.
Finset.inter_sdiff_assoc theorem
(s t u : Finset α) : (s ∩ t) \ u = s ∩ (t \ u)
Full source 
/-- See also `Finset.sdiff_inter_right_comm`. -/
lemma inter_sdiff_assoc (s t u : Finset α) : (s ∩ t) \ u = s ∩ (t \ u) := inf_sdiff_assoc ..
Associativity of Intersection with Set Difference for Finite Sets
Informal description
For any finite sets $s$, $t$, and $u$ of type $\alpha$, the set difference of the intersection $s \cap t$ with $u$ is equal to the intersection of $s$ with the set difference $t \setminus u$. That is: $$ (s \cap t) \setminus u = s \cap (t \setminus u). $$
Finset.sdiff_inter_right_comm theorem
(s t u : Finset α) : s \ t ∩ u = (s ∩ u) \ t
Full source 
/-- See also `Finset.inter_sdiff_assoc`. -/
lemma sdiff_inter_right_comm (s t u : Finset α) : s \ ts \ t ∩ u = (s ∩ u) \ t := sdiff_inf_right_comm ..
Right Commutativity of Intersection with Set Difference for Finite Sets: $(s \setminus t) \cap u = (s \cap u) \setminus t$
Informal description
For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the intersection of the set difference $s \setminus t$ with $u$ is equal to the set difference of the intersection $s \cap u$ with $t$. That is: $$ (s \setminus t) \cap u = (s \cap u) \setminus t. $$
Finset.inter_sdiff_left_comm theorem
(s t u : Finset α) : s ∩ (t \ u) = t ∩ (s \ u)
Full source 
lemma inter_sdiff_left_comm (s t u : Finset α) : s ∩ (t \ u) = t ∩ (s \ u) := inf_sdiff_left_comm ..
Left Commutativity of Intersection with Set Difference in Finite Sets
Informal description
For any finite sets $s$, $t$, and $u$ of type $\alpha$, the following equality holds: \[ s \cap (t \setminus u) = t \cap (s \setminus u). \]
Finset.sdiff_inter_self theorem
(s₁ s₂ : Finset α) : s₂ \ s₁ ∩ s₁ = ∅
Full source 
@[simp]
theorem sdiff_inter_self (s₁ s₂ : Finset α) : s₂ \ s₁s₂ \ s₁ ∩ s₁ = ∅ :=
  inf_sdiff_self_left
Annihilation of Intersection with Set Difference in Finite Sets: $(s_2 \setminus s_1) \cap s_1 = \emptyset$
Informal description
For any two finite sets $s_1$ and $s_2$ of a type $\alpha$, the intersection of the set difference $s_2 \setminus s_1$ with $s_1$ is empty, i.e., $$ (s_2 \setminus s_1) \cap s_1 = \emptyset. $$
Finset.sdiff_self theorem
(s₁ : Finset α) : s₁ \ s₁ = ∅
Full source 
protected theorem sdiff_self (s₁ : Finset α) : s₁ \ s₁ = ∅ :=
  _root_.sdiff_self
Self-Difference of Finite Set is Empty: $s \setminus s = \emptyset$
Informal description
For any finite set $s_1$ of elements of type $\alpha$, the set difference $s_1 \setminus s_1$ is equal to the empty set $\emptyset$.
Finset.sdiff_inter_distrib_right theorem
(s t u : Finset α) : s \ (t ∩ u) = s \ t ∪ s \ u
Full source 
theorem sdiff_inter_distrib_right (s t u : Finset α) : s \ (t ∩ u) = s \ ts \ t ∪ s \ u :=
  sdiff_inf
Distributivity of Set Difference over Intersection in Finite Sets
Informal description
For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the set difference of $s$ with the intersection of $t$ and $u$ is equal to the union of the set differences $s \setminus t$ and $s \setminus u$, i.e., $$ s \setminus (t \cap u) = (s \setminus t) \cup (s \setminus u). $$
Finset.sdiff_inter_self_left theorem
(s t : Finset α) : s \ (s ∩ t) = s \ t
Full source 
@[simp]
theorem sdiff_inter_self_left (s t : Finset α) : s \ (s ∩ t) = s \ t :=
  sdiff_inf_self_left _ _
Difference of Finite Set with Its Intersection: $s \setminus (s \cap t) = s \setminus t$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the set difference of $s$ with the intersection of $s$ and $t$ equals the set difference of $s$ and $t$, i.e., $$ s \setminus (s \cap t) = s \setminus t. $$
Finset.sdiff_inter_self_right theorem
(s t : Finset α) : s \ (t ∩ s) = s \ t
Full source 
@[simp]
theorem sdiff_inter_self_right (s t : Finset α) : s \ (t ∩ s) = s \ t :=
  sdiff_inf_self_right _ _
Right Self-Intersection Difference Identity: $s \setminus (t \cap s) = s \setminus t$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the set difference $s \setminus (t \cap s)$ equals $s \setminus t$.
Finset.sdiff_empty theorem
: s \ ∅ = s
Full source 
@[simp]
theorem sdiff_empty : s \ ∅ = s :=
  sdiff_bot
Set Difference with Empty Set: $s \setminus \emptyset = s$
Informal description
For any finite set $s$ of type $\alpha$, the set difference $s \setminus \emptyset$ equals $s$, i.e., $s \setminus \emptyset = s$.
Finset.sdiff_subset_sdiff theorem
(hst : s ⊆ t) (hvu : v ⊆ u) : s \ u ⊆ t \ v
Full source 
@[mono, gcongr]
theorem sdiff_subset_sdiff (hst : s ⊆ t) (hvu : v ⊆ u) : s \ us \ u ⊆ t \ v :=
  subset_of_le (sdiff_le_sdiff hst hvu)
Monotonicity of Set Difference: $s \subseteq t \land v \subseteq u \Rightarrow s \setminus u \subseteq t \setminus v$
Informal description
For any finite sets $s, t, u, v$ of a type $\alpha$, if $s \subseteq t$ and $v \subseteq u$, then the set difference $s \setminus u$ is a subset of $t \setminus v$.
Finset.sdiff_subset_sdiff_iff_subset theorem
{r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) : r \ s ⊆ r \ t ↔ t ⊆ s
Full source 
theorem sdiff_subset_sdiff_iff_subset {r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) :
    r \ sr \ s ⊆ r \ tr \ s ⊆ r \ t ↔ t ⊆ s := by
  simpa only [← le_eq_subset] using sdiff_le_sdiff_iff_le hs ht
Relative Complement Order Reversal for Finite Sets: $r \setminus s \subseteq r \setminus t \leftrightarrow t \subseteq s$ under $s, t \subseteq r$
Informal description
For any finite sets $s$, $t$, and $r$ of a type $\alpha$, if $s \subseteq r$ and $t \subseteq r$, then the set difference $r \setminus s$ is a subset of $r \setminus t$ if and only if $t \subseteq s$.
Finset.coe_sdiff theorem
(s₁ s₂ : Finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : Set α)
Full source 
@[simp, norm_cast]
theorem coe_sdiff (s₁ s₂ : Finset α) : ↑(s₁ \ s₂) = (s₁ \ s₂ : Set α) :=
  Set.ext fun _ => mem_sdiff
Coercion Preserves Set Difference for Finite Sets: $\overline{s₁ \setminus s₂} = \overline{s₁} \setminus \overline{s₂}$
Informal description
For any finite sets $s₁$ and $s₂$ of type $\alpha$, the coercion of their set difference $s₁ \setminus s₂$ to a set is equal to the set difference of their coercions, i.e., $(s₁ \setminus s₂ : \text{Set } \alpha) = (s₁ : \text{Set } \alpha) \setminus (s₂ : \text{Set } \alpha)$.
Finset.union_sdiff_self_eq_union theorem
: s ∪ t \ s = s ∪ t
Full source 
@[simp]
theorem union_sdiff_self_eq_union : s ∪ t \ s = s ∪ t :=
  sup_sdiff_self_right _ _
Union with Set Difference Equals Union
Informal description
For any finite sets $s$ and $t$, the union of $s$ with the set difference $t \setminus s$ is equal to the union of $s$ and $t$, i.e., $s \cup (t \setminus s) = s \cup t$.
Finset.sdiff_union_self_eq_union theorem
: s \ t ∪ t = s ∪ t
Full source 
@[simp]
theorem sdiff_union_self_eq_union : s \ ts \ t ∪ t = s ∪ t :=
  sup_sdiff_self_left _ _
Union-Difference Identity for Finite Sets: $(s \setminus t) \cup t = s \cup t$
Informal description
For any finite sets $s$ and $t$ of type $\alpha$, the union of the set difference $s \setminus t$ with $t$ equals the union of $s$ and $t$, i.e., $(s \setminus t) \cup t = s \cup t$.
Finset.union_sdiff_left theorem
(s t : Finset α) : (s ∪ t) \ s = t \ s
Full source 
theorem union_sdiff_left (s t : Finset α) : (s ∪ t) \ s = t \ s :=
  sup_sdiff_left_self
Left Union-Difference Identity for Finite Sets: $(s \cup t) \setminus s = t \setminus s$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the set difference of their union with $s$ equals the set difference of $t$ with $s$, i.e., $(s \cup t) \setminus s = t \setminus s$.
Finset.union_sdiff_right theorem
(s t : Finset α) : (s ∪ t) \ t = s \ t
Full source 
theorem union_sdiff_right (s t : Finset α) : (s ∪ t) \ t = s \ t :=
  sup_sdiff_right_self
Right Union-Difference Identity for Finite Sets: $(s \cup t) \setminus t = s \setminus t$
Informal description
For any finite sets $s$ and $t$ of type $\alpha$, the set difference of their union with $t$ equals the set difference of $s$ with $t$, i.e., $(s \cup t) \setminus t = s \setminus t$.
Finset.union_sdiff_cancel_left theorem
(h : Disjoint s t) : (s ∪ t) \ s = t
Full source 
theorem union_sdiff_cancel_left (h : Disjoint s t) : (s ∪ t) \ s = t :=
  h.sup_sdiff_cancel_left
Left Cancellation of Union with Difference for Disjoint Finite Sets: $(s \cup t) \setminus s = t$ when $s \cap t = \emptyset$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$), then the set difference of their union with $s$ equals $t$, i.e., $(s \cup t) \setminus s = t$.
Finset.union_sdiff_cancel_right theorem
(h : Disjoint s t) : (s ∪ t) \ t = s
Full source 
theorem union_sdiff_cancel_right (h : Disjoint s t) : (s ∪ t) \ t = s :=
  h.sup_sdiff_cancel_right
Right Cancellation of Union with Difference for Disjoint Finite Sets: $(s \cup t) \setminus t = s$ when $s \cap t = \emptyset$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$), then the set difference of their union with $t$ equals $s$, i.e., $(s \cup t) \setminus t = s$.
Finset.union_sdiff_symm theorem
: s ∪ t \ s = t ∪ s \ t
Full source 
theorem union_sdiff_symm : s ∪ t \ s = t ∪ s \ t := by simp [union_comm]
Symmetric Property of Union with Set Difference: $s \cup (t \setminus s) = t \cup (s \setminus t)$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the union of $s$ with the set difference $t \setminus s$ is equal to the union of $t$ with the set difference $s \setminus t$, i.e., $s \cup (t \setminus s) = t \cup (s \setminus t)$.
Finset.sdiff_union_inter theorem
(s t : Finset α) : s \ t ∪ s ∩ t = s
Full source 
theorem sdiff_union_inter (s t : Finset α) : s \ ts \ t ∪ s ∩ t = s :=
  sup_sdiff_inf _ _
Decomposition of Finite Set via Difference and Intersection: $(s \setminus t) \cup (s \cap t) = s$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the union of the set difference $s \setminus t$ and the intersection $s \cap t$ equals $s$, i.e., $(s \setminus t) \cup (s \cap t) = s$.
Finset.sdiff_idem theorem
(s t : Finset α) : (s \ t) \ t = s \ t
Full source 
theorem sdiff_idem (s t : Finset α) : (s \ t) \ t = s \ t :=
  _root_.sdiff_idem
Idempotence of Finite Set Difference: $(s \setminus t) \setminus t = s \setminus t$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the double set difference operation satisfies $(s \setminus t) \setminus t = s \setminus t$.
Finset.subset_sdiff theorem
: s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
Full source 
theorem subset_sdiff : s ⊆ t \ us ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u :=
  le_iff_subset.symm.trans le_sdiff
Subset Characterization via Set Difference and Disjointness: $s \subseteq t \setminus u \leftrightarrow (s \subseteq t \land s \perp u)$
Informal description
For any finite sets $s, t, u$ of a type $\alpha$, the subset relation $s \subseteq t \setminus u$ holds if and only if $s \subseteq t$ and $s$ is disjoint from $u$.
Finset.sdiff_eq_empty_iff_subset theorem
: s \ t = ∅ ↔ s ⊆ t
Full source 
@[simp]
theorem sdiff_eq_empty_iff_subset : s \ ts \ t = ∅ ↔ s ⊆ t :=
  sdiff_eq_bot_iff
Empty Difference Condition for Finite Sets: $s \setminus t = \emptyset \leftrightarrow s \subseteq t$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the set difference $s \setminus t$ is empty if and only if $s$ is a subset of $t$.
Finset.empty_sdiff theorem
(s : Finset α) : ∅ \ s = ∅
Full source 
@[simp]
theorem empty_sdiff (s : Finset α) : ∅∅ \ s = ∅ :=
  bot_sdiff
Empty Set Difference Identity: $\emptyset \setminus s = \emptyset$
Informal description
For any finite set $s$ of type $\alpha$, the set difference between the empty set $\emptyset$ and $s$ is equal to $\emptyset$, i.e., $\emptyset \setminus s = \emptyset$.
Finset.insert_sdiff_of_not_mem theorem
(s : Finset α) {t : Finset α} {x : α} (h : x ∉ t) : insert x s \ t = insert x (s \ t)
Full source 
theorem insert_sdiff_of_not_mem (s : Finset α) {t : Finset α} {x : α} (h : x ∉ t) :
    insertinsert x s \ t = insert x (s \ t) := by
  rw [← coe_inj, coe_insert, coe_sdiff, coe_sdiff, coe_insert]
  exact Set.insert_diff_of_not_mem _ h
Insertion and Set Difference for Non-Member Elements in Finite Sets: $\{x\} \cup s \setminus t = \{x\} \cup (s \setminus t)$ when $x \notin t$
Informal description
For any finite set $s$ of type $\alpha$, any finite set $t$ of type $\alpha$, and any element $x$ of type $\alpha$ such that $x \notin t$, the set difference between $\{x\} \cup s$ and $t$ is equal to $\{x\} \cup (s \setminus t)$. In symbols: $$\{x\} \cup s \setminus t = \{x\} \cup (s \setminus t)$$
Finset.insert_sdiff_of_mem theorem
(s : Finset α) {x : α} (h : x ∈ t) : insert x s \ t = s \ t
Full source 
theorem insert_sdiff_of_mem (s : Finset α) {x : α} (h : x ∈ t) : insertinsert x s \ t = s \ t := by
  rw [← coe_inj, coe_sdiff, coe_sdiff, coe_insert]
  exact Set.insert_diff_of_mem _ h
Set Difference with Insertion of an Element Already in the Second Set
Informal description
For any finite set $s$ of type $\alpha$, element $x \in \alpha$, and finite set $t$ of type $\alpha$, if $x \in t$, then the set difference between $\{x\} \cup s$ and $t$ is equal to the set difference between $s$ and $t$, i.e., $(x \cup s) \setminus t = s \setminus t$.
Finset.insert_sdiff_cancel theorem
(ha : a ∉ s) : insert a s \ s = { a }
Full source 
@[simp] lemma insert_sdiff_cancel (ha : a ∉ s) : insertinsert a s \ s = {a} := by
  rw [insert_sdiff_of_not_mem _ ha, Finset.sdiff_self, insert_empty_eq]
Set Difference Cancellation for Inserted Element: $(\{a\} \cup s) \setminus s = \{a\}$ when $a \notin s$
Informal description
For any finite set $s$ of type $\alpha$ and any element $a \in \alpha$ such that $a \notin s$, the set difference between $\{a\} \cup s$ and $s$ is the singleton set $\{a\}$, i.e., $(\{a\} \cup s) \setminus s = \{a\}$.
Finset.insert_sdiff_insert theorem
(s t : Finset α) (x : α) : insert x s \ insert x t = s \ insert x t
Full source 
@[simp]
theorem insert_sdiff_insert (s t : Finset α) (x : α) : insertinsert x s \ insert x t = s \ insert x t :=
  insert_sdiff_of_mem _ (mem_insert_self _ _)
Set Difference with Insertion of Same Element: $(x \cup s) \setminus (x \cup t) = s \setminus (x \cup t)$
Informal description
For any finite sets $s$ and $t$ of type $\alpha$ and any element $x \in \alpha$, the set difference between $\{x\} \cup s$ and $\{x\} \cup t$ is equal to the set difference between $s$ and $\{x\} \cup t$, i.e., $(x \cup s) \setminus (x \cup t) = s \setminus (x \cup t)$.
Finset.insert_sdiff_insert' theorem
(hab : a ≠ b) (ha : a ∉ s) : insert a s \ insert b s = { a }
Full source 
lemma insert_sdiff_insert' (hab : a ≠ b) (ha : a ∉ s) : insertinsert a s \ insert b s = {a} := by
  ext; aesop
Set Difference of Insertions with Distinct Elements: $(\{a\} \cup s) \setminus (\{b\} \cup s) = \{a\}$
Informal description
For any two distinct elements $a$ and $b$ of a type $\alpha$, and any finite set $s$ of $\alpha$ such that $a \notin s$, the set difference between $\{a\} \cup s$ and $\{b\} \cup s$ is the singleton set $\{a\}$, i.e., $(\{a\} \cup s) \setminus (\{b\} \cup s) = \{a\}$.
Finset.cons_sdiff_cons theorem
(hab : a ≠ b) (ha hb) : s.cons a ha \ s.cons b hb = { a }
Full source 
lemma cons_sdiff_cons (hab : a ≠ b) (ha hb) : s.cons a ha \ s.cons b hb = {a} := by
  rw [cons_eq_insert, cons_eq_insert, insert_sdiff_insert' hab ha]
Set Difference of Cons Operations with Distinct Elements: $(\{a\} \cup s) \setminus (\{b\} \cup s) = \{a\}$
Informal description
For any two distinct elements $a$ and $b$ of a type $\alpha$, and any finite set $s$ of $\alpha$ with proofs $ha : a \notin s$ and $hb : b \notin s$, the set difference between $\{a\} \cup s$ and $\{b\} \cup s$ is the singleton set $\{a\}$, i.e., $(\{a\} \cup s) \setminus (\{b\} \cup s) = \{a\}$.
Finset.sdiff_insert_of_not_mem theorem
{x : α} (h : x ∉ s) (t : Finset α) : s \ insert x t = s \ t
Full source 
theorem sdiff_insert_of_not_mem {x : α} (h : x ∉ s) (t : Finset α) : s \ insert x t = s \ t := by
  refine Subset.antisymm (sdiff_subset_sdiff (Subset.refl _) (subset_insert _ _)) fun y hy => ?_
  simp only [mem_sdiff, mem_insert, not_or] at hy ⊢
  exact ⟨hy.1, fun hxy => h <| hxy ▸ hy.1, hy.2⟩
Set Difference with Insertion of Non-Member Element: $s \setminus (t \cup \{x\}) = s \setminus t$ when $x \notin s$
Informal description
For any element $x$ of type $\alpha$ not in a finite set $s$, and any finite set $t$ of $\alpha$, the set difference $s \setminus (\{x\} \cup t)$ is equal to $s \setminus t$.
Finset.sdiff_subset theorem
{s t : Finset α} : s \ t ⊆ s
Full source 
@[simp] theorem sdiff_subset {s t : Finset α} : s \ ts \ t ⊆ s := le_iff_subset.mp sdiff_le
Set Difference is Subset of Original Finite Set
Informal description
For any two finite sets $s$ and $t$ of a type $\alpha$, the set difference $s \setminus t$ is a subset of $s$, i.e., $s \setminus t \subseteq s$.
Finset.sdiff_ssubset theorem
(h : t ⊆ s) (ht : t.Nonempty) : s \ t ⊂ s
Full source 
theorem sdiff_ssubset (h : t ⊆ s) (ht : t.Nonempty) : s \ ts \ t ⊂ s :=
  sdiff_lt (le_iff_subset.mpr h) ht.ne_empty
Strict Subset Property for Nonempty Set Difference: $t \subseteq s \land t \neq \emptyset \implies s \setminus t \subset s$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, if $t$ is a nonempty subset of $s$, then the set difference $s \setminus t$ is a strict subset of $s$, i.e., $s \setminus t \subset s$.
Finset.union_sdiff_distrib theorem
(s₁ s₂ t : Finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t
Full source 
theorem union_sdiff_distrib (s₁ s₂ t : Finset α) : (s₁ ∪ s₂) \ t = s₁ \ ts₁ \ t ∪ s₂ \ t :=
  sup_sdiff
Distributivity of Set Difference over Union for Finite Sets
Informal description
For any finite sets $s_1$, $s_2$, and $t$ of elements of type $\alpha$, the set difference of the union $s_1 \cup s_2$ with $t$ is equal to the union of the set differences $s_1 \setminus t$ and $s_2 \setminus t$, i.e., $$(s_1 \cup s_2) \setminus t = (s_1 \setminus t) \cup (s_2 \setminus t).$$
Finset.sdiff_union_distrib theorem
(s t₁ t₂ : Finset α) : s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)
Full source 
theorem sdiff_union_distrib (s t₁ t₂ : Finset α) : s \ (t₁ ∪ t₂) = s \ t₁s \ t₁ ∩ (s \ t₂) :=
  sdiff_sup
Distributivity of Set Difference over Union via Intersection for Finite Sets
Informal description
For any finite sets $s$, $t_1$, and $t_2$ of elements of type $\alpha$, the set difference of $s$ with the union $t_1 \cup t_2$ equals the intersection of the set differences $s \setminus t_1$ and $s \setminus t_2$, i.e., $$ s \setminus (t_1 \cup t_2) = (s \setminus t_1) \cap (s \setminus t_2). $$
Finset.union_sdiff_self theorem
(s t : Finset α) : (s ∪ t) \ t = s \ t
Full source 
theorem union_sdiff_self (s t : Finset α) : (s ∪ t) \ t = s \ t :=
  sup_sdiff_right_self
Right Self-Difference Identity for Finite Sets: $(s \cup t) \setminus t = s \setminus t$
Informal description
For any finite sets $s$ and $t$ of elements of type $\alpha$, the set difference of their union with $t$ equals the set difference of $s$ with $t$, i.e., $(s \cup t) \setminus t = s \setminus t$.
Finset.Nontrivial.sdiff_singleton_nonempty theorem
{c : α} {s : Finset α} (hS : s.Nontrivial) : (s \ { c }).Nonempty
Full source 
theorem Nontrivial.sdiff_singleton_nonempty {c : α} {s : Finset α} (hS : s.Nontrivial) :
    (s \ {c}).Nonempty := by
  rw [Finset.sdiff_nonempty, Finset.subset_singleton_iff]
  push_neg
  exact ⟨by rintro rfl; exact Finset.not_nontrivial_empty hS, hS.ne_singleton⟩
Nonempty Difference from Nontrivial Finite Set after Removing a Singleton
Informal description
For any finite set $s$ of type $\alpha$ and any element $c \in \alpha$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then the set difference $s \setminus \{c\}$ is nonempty.
Finset.sdiff_sdiff_left' theorem
(s t u : Finset α) : (s \ t) \ u = s \ t ∩ (s \ u)
Full source 
theorem sdiff_sdiff_left' (s t u : Finset α) : (s \ t) \ u = s \ ts \ t ∩ (s \ u) :=
  _root_.sdiff_sdiff_left'
Double Set Difference as Intersection of Differences for Finite Sets
Informal description
For any finite sets $s$, $t$, and $u$ of a type $\alpha$, the double set difference $(s \setminus t) \setminus u$ equals the intersection of the set differences $s \setminus t$ and $s \setminus u$, i.e., $$ (s \setminus t) \setminus u = (s \setminus t) \cap (s \setminus u). $$
Finset.sdiff_union_sdiff_cancel theorem
(hts : t ⊆ s) (hut : u ⊆ t) : s \ t ∪ t \ u = s \ u
Full source 
theorem sdiff_union_sdiff_cancel (hts : t ⊆ s) (hut : u ⊆ t) : s \ ts \ t ∪ t \ u = s \ u :=
  sdiff_sup_sdiff_cancel hts hut
Cancellation Law for Set Differences: $(s \setminus t) \cup (t \setminus u) = s \setminus u$ under $t \subseteq s$ and $u \subseteq t$
Informal description
For any finite sets $s$, $t$, and $u$ of a type $\alpha$, if $t \subseteq s$ and $u \subseteq t$, then $(s \setminus t) \cup (t \setminus u) = s \setminus u$.
Finset.sdiff_sdiff_eq_sdiff_union theorem
(h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u
Full source 
theorem sdiff_sdiff_eq_sdiff_union (h : u ⊆ s) : s \ (t \ u) = s \ ts \ t ∪ u :=
  sdiff_sdiff_eq_sdiff_sup h
Double Set Difference Identity under Subset Condition: $s \setminus (t \setminus u) = (s \setminus t) \cup u$ when $u \subseteq s$
Informal description
For any finite sets $s$, $t$, and $u$ of a type $\alpha$, if $u \subseteq s$, then the set difference $s \setminus (t \setminus u)$ equals the union of the set difference $s \setminus t$ and the set $u$, i.e., $$ s \setminus (t \setminus u) = (s \setminus t) \cup u. $$
Finset.sdiff_sdiff_self_left theorem
(s t : Finset α) : s \ (s \ t) = s ∩ t
Full source 
theorem sdiff_sdiff_self_left (s t : Finset α) : s \ (s \ t) = s ∩ t :=
  sdiff_sdiff_right_self
Double Set Difference Equals Intersection: $s \setminus (s \setminus t) = s \cap t$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, the set difference $s \setminus (s \setminus t)$ equals the intersection $s \cap t$.
Finset.sdiff_sdiff_eq_self theorem
(h : t ⊆ s) : s \ (s \ t) = t
Full source 
theorem sdiff_sdiff_eq_self (h : t ⊆ s) : s \ (s \ t) = t :=
  _root_.sdiff_sdiff_eq_self h
Double Set Difference Cancellation: $s \setminus (s \setminus t) = t$ when $t \subseteq s$
Informal description
For any finite sets $s$ and $t$ of a type $\alpha$, if $t$ is a subset of $s$, then the set difference $s \setminus (s \setminus t)$ equals $t$, i.e., $$ s \setminus (s \setminus t) = t. $$
Finset.sdiff_eq_sdiff_iff_inter_eq_inter theorem
{s t₁ t₂ : Finset α} : s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂
Full source 
theorem sdiff_eq_sdiff_iff_inter_eq_inter {s t₁ t₂ : Finset α} :
    s \ t₁s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂ :=
  sdiff_eq_sdiff_iff_inf_eq_inf
Equality of Set Differences via Intersection Equality: $s \setminus t_1 = s \setminus t_2 \iff s \cap t_1 = s \cap t_2$
Informal description
For any finite sets $s, t_1, t_2$ of type $\alpha$, the set differences $s \setminus t_1$ and $s \setminus t_2$ are equal if and only if the intersections $s \cap t_1$ and $s \cap t_2$ are equal. That is, $$ s \setminus t_1 = s \setminus t_2 \iff s \cap t_1 = s \cap t_2. $$
Finset.union_eq_sdiff_union_sdiff_union_inter theorem
(s t : Finset α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
Full source 
theorem union_eq_sdiff_union_sdiff_union_inter (s t : Finset α) : s ∪ t = s \ ts \ t ∪ t \ ss \ t ∪ t \ s ∪ s ∩ t :=
  sup_eq_sdiff_sup_sdiff_sup_inf
Decomposition of Union into Differences and Intersection for Finite Sets
Informal description
For any two finite sets $s$ and $t$ of type $\alpha$, the union $s \cup t$ can be expressed as the union of their set differences and their intersection, i.e., $$ s \cup t = (s \setminus t) \cup (t \setminus s) \cup (s \cap t). $$
Finset.sdiff_eq_self_iff_disjoint theorem
: s \ t = s ↔ Disjoint s t
Full source 
theorem sdiff_eq_self_iff_disjoint : s \ ts \ t = s ↔ Disjoint s t :=
  sdiff_eq_self_iff_disjoint'
Set Difference Equals Original Set if and Only if Disjoint: $s \setminus t = s \iff s \cap t = \emptyset$
Informal description
For any finite sets $s$ and $t$ of type $\alpha$, the set difference $s \setminus t$ equals $s$ if and only if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$).
Finset.sdiff_eq_self_of_disjoint theorem
(h : Disjoint s t) : s \ t = s
Full source 
theorem sdiff_eq_self_of_disjoint (h : Disjoint s t) : s \ t = s :=
  sdiff_eq_self_iff_disjoint.2 h
Set Difference Equals Original Set for Disjoint Finite Sets: $s \setminus t = s$ when $s \cap t = \emptyset$
Informal description
For any two finite sets $s$ and $t$ of type $\alpha$, if $s$ and $t$ are disjoint (i.e., $s \cap t = \emptyset$), then the set difference $s \setminus t$ equals $s$.