Documentation

Mathlib.Data.Finset.SDiff

Difference of finite sets #

Main declarations #

Tags #

finite sets, finset

sdiff #

source
instance Finset.instSDiff {α : Type u_1} [DecidableEq α] :
SDiff (Finset α)

s \ t is the set consisting of the elements of s that are not in t.

Equations
  • Finset.instSDiff = { sdiff := fun (s₁ s₂ : Finset α) => { val := s₁.val - s₂.val, nodup := ⋯ } }
source
@[simp]
theorem Finset.sdiff_val {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
(s₁ \ s₂).val = s₁.val - s₂.val
source
@[simp]
theorem Finset.mem_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
a ∈ s \ t ↔ a ∈ s ∧ a ∉ t
source
@[simp]
theorem Finset.inter_sdiff_self {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
s₁ ∩ (s₂ \ s₁) = ∅
source
instance Finset.instGeneralizedBooleanAlgebra {α : Type u_1} [DecidableEq α] :
GeneralizedBooleanAlgebra (Finset α)
Equations
source
theorem Finset.not_mem_sdiff_of_mem_right {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∈ t) :
a ∉ s \ t
source
theorem Finset.not_mem_sdiff_of_not_mem_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∉ s) :
a ∉ s \ t
source
theorem Finset.union_sdiff_of_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) :
s ∪ t \ s = t
source
theorem Finset.sdiff_union_of_subset {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) :
s₂ \ s₁ ∪ s₁ = s₂
source
theorem Finset.inter_sdiff_assoc {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
(s ∩ t) \ u = s ∩ (t \ u)
source
@[deprecated Finset.inter_sdiff_assoc]
theorem Finset.inter_sdiff {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s ∩ (t \ u) = (s ∩ t) \ u
source
@[simp]
theorem Finset.sdiff_inter_self {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
s₂ \ s₁ ∩ s₁ = ∅
source
theorem Finset.sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) :
s₁ \ s₁ = ∅
source
theorem Finset.sdiff_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
s \ (t ∩ u) = s \ t ∪ s \ u
source
@[simp]
theorem Finset.sdiff_inter_self_left {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s \ (s ∩ t) = s \ t
source
@[simp]
theorem Finset.sdiff_inter_self_right {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s \ (t ∩ s) = s \ t
source
@[simp]
theorem Finset.sdiff_empty {α : Type u_1} [DecidableEq α] {s : Finset α} :
s \ ∅ = s
source
theorem Finset.sdiff_subset_sdiff {α : Type u_1} [DecidableEq α] {s t u v : Finset α} (hst : s ⊆ t) (hvu : v ⊆ u) :
s \ u ⊆ t \ v
source
theorem Finset.sdiff_subset_sdiff_iff_subset {α : Type u_1} [DecidableEq α] {s t r : Finset α} (hs : s ⊆ r) (ht : t ⊆ r) :
r \ s ⊆ r \ t ↔ t ⊆ s
source
@[simp]
theorem Finset.coe_sdiff {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
↑(s₁ \ s₂) = ↑s₁ \ ↑s₂
source
@[simp]
theorem Finset.union_sdiff_self_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∪ t \ s = s ∪ t
source
@[simp]
theorem Finset.sdiff_union_self_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s \ t ∪ t = s ∪ t
source
theorem Finset.union_sdiff_left {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t) \ s = t \ s
source
theorem Finset.union_sdiff_right {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t) \ t = s \ t
source
theorem Finset.union_sdiff_cancel_left {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) :
(s ∪ t) \ s = t
source
theorem Finset.union_sdiff_cancel_right {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) :
(s ∪ t) \ t = s
source
theorem Finset.union_sdiff_symm {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s ∪ t \ s = t ∪ s \ t
source
theorem Finset.sdiff_union_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s \ t ∪ s ∩ t = s
source
theorem Finset.sdiff_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s \ t) \ t = s \ t
source
theorem Finset.subset_sdiff {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
source
@[simp]
theorem Finset.sdiff_eq_empty_iff_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s \ t = ∅ ↔ s ⊆ t
source
theorem Finset.sdiff_nonempty {α : Type u_1} [DecidableEq α] {s t : Finset α} :
(s \ t).Nonempty ↔ ¬s ⊆ t
source
@[simp]
theorem Finset.empty_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) :
∅ \ s = ∅
source
theorem Finset.insert_sdiff_of_not_mem {α : Type u_1} [DecidableEq α] (s : Finset α) {t : Finset α} {x : α} (h : x ∉ t) :
insert x s \ t = insert x (s \ t)
source
theorem Finset.insert_sdiff_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} (s : Finset α) {x : α} (h : x ∈ t) :
insert x s \ t = s \ t
source
@[simp]
theorem Finset.insert_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∉ s) :
insert a s \ s = {a}
source
@[simp]
theorem Finset.insert_sdiff_insert {α : Type u_1} [DecidableEq α] (s t : Finset α) (x : α) :
insert x s \ insert x t = s \ insert x t
source
theorem Finset.insert_sdiff_insert' {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hab : a ≠ b) (ha : a ∉ s) :
insert a s \ insert b s = {a}
source
theorem Finset.cons_sdiff_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hab : a ≠ b) (ha : a ∉ s) (hb : b ∉ s) :
Finset.cons a s ha \ Finset.cons b s hb = {a}
source
theorem Finset.sdiff_insert_of_not_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} (h : x ∉ s) (t : Finset α) :
s \ insert x t = s \ t
source
@[simp]
theorem Finset.sdiff_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s \ t ⊆ s
source
theorem Finset.sdiff_ssubset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t ⊆ s) (ht : t.Nonempty) :
s \ t ⊂ s
source
theorem Finset.union_sdiff_distrib {α : Type u_1} [DecidableEq α] (s₁ s₂ t : Finset α) :
(s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t
source
theorem Finset.sdiff_union_distrib {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) :
s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)
source
theorem Finset.union_sdiff_self {α : Type u_1} [DecidableEq α] (s t : Finset α) :
(s ∪ t) \ t = s \ t
source
theorem Finset.Nontrivial.sdiff_singleton_nonempty {α : Type u_1} [DecidableEq α] {c : α} {s : Finset α} (hS : s.Nontrivial) :
(s \ {c}).Nonempty
source
theorem Finset.sdiff_sdiff_left' {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
(s \ t) \ u = s \ t ∩ (s \ u)
source
theorem Finset.sdiff_union_sdiff_cancel {α : Type u_1} [DecidableEq α] {s t u : Finset α} (hts : t ⊆ s) (hut : u ⊆ t) :
s \ t ∪ t \ u = s \ u
source
theorem Finset.sdiff_sdiff_eq_sdiff_union {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : u ⊆ s) :
s \ (t \ u) = s \ t ∪ u
source
theorem Finset.sdiff_sdiff_self_left {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s \ (s \ t) = s ∩ t
source
theorem Finset.sdiff_sdiff_eq_self {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t ⊆ s) :
s \ (s \ t) = t
source
theorem Finset.sdiff_eq_sdiff_iff_inter_eq_inter {α : Type u_1} [DecidableEq α] {s t₁ t₂ : Finset α} :
s \ t₁ = s \ t₂ ↔ s ∩ t₁ = s ∩ t₂
source
theorem Finset.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
s ∪ t = s \ t ∪ t \ s ∪ s ∩ t
source
theorem Finset.sdiff_eq_self_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s \ t = s ↔ Disjoint s t
source
@[deprecated Finset.sdiff_eq_self_iff_disjoint]
theorem Finset.sdiff_eq_self {α : Type u_1} [DecidableEq α] {s t : Finset α} :
s \ t = s ↔ Disjoint s t

Alias of Finset.sdiff_eq_self_iff_disjoint.

source
theorem Finset.sdiff_eq_self_of_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) :
s \ t = s