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

@[instance_reducible]

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 := ⋯ } }

@[simp]

theorem Finset.sdiff_val {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : (s₁ \ s₂).val = s₁.val - s₂.val

@[simp]

theorem Finset.mem_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} : a ∈ s \ t ↔ a ∈ s ∧ a ∉ t

@[simp]

theorem Finset.inter_sdiff_self {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : s₁ ∩ (s₂ \ s₁) = ∅

@[instance_reducible]

instance Finset.instGeneralizedBooleanAlgebra {α : Type u_1} [DecidableEq α] : GeneralizedBooleanAlgebra (Finset α)

Equations

• Finset.instGeneralizedBooleanAlgebra = { toDistribLattice := Finset.instDistribLattice, toSDiff := Finset.instSDiff, toBot := Finset.instOrderBot.toBot, sup_inf_sdiff := ⋯, inf_inf_sdiff := ⋯ }

theorem Finset.notMem_sdiff_of_mem_right {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∈ t) : a ∉ s \ t

theorem Finset.notMem_sdiff_of_notMem_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∉ s) : a ∉ s \ t

theorem Finset.union_sdiff_of_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) : s ∪ t \ s = t

theorem Finset.sdiff_union_of_subset {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) : s₂ \ s₁ ∪ s₁ = s₂

theorem Finset.inter_sdiff_assoc {α : Type u_1} [DecidableEq α] (s t u : Finset α) : (s ∩ t) \ u = s ∩ (t \ u)

See also Finset.sdiff_inter_right_comm.

theorem Finset.sdiff_inter_right_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s \ t ∩ u = (s ∩ u) \ t

See also Finset.inter_sdiff_assoc.

theorem Finset.inter_sdiff_left_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s ∩ (t \ u) = t ∩ (s \ u)

@[simp]

theorem Finset.sdiff_inter_self {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : s₂ \ s₁ ∩ s₁ = ∅

theorem Finset.sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) : s₁ \ s₁ = ∅

theorem Finset.sdiff_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) : s \ (t ∩ u) = s \ t ∪ s \ u

@[simp]

theorem Finset.sdiff_inter_self_left {α : Type u_1} [DecidableEq α] (s t : Finset α) : s \ (s ∩ t) = s \ t

@[simp]

theorem Finset.sdiff_inter_self_right {α : Type u_1} [DecidableEq α] (s t : Finset α) : s \ (t ∩ s) = s \ t

@[simp]

theorem Finset.sdiff_empty {α : Type u_1} [DecidableEq α] {s : Finset α} : s \ ∅ = s

theorem Finset.sdiff_subset_sdiff {α : Type u_1} [DecidableEq α] {s t u v : Finset α} (hst : s ⊆ t) (hvu : v ⊆ u) : s \ u ⊆ t \ v

theorem Finset.sdiff_subset_sdiff_left {α : Type u_1} [DecidableEq α] {s t : Finset α} (u : Finset α) (h : s ⊆ t) : s \ u ⊆ t \ u

theorem Finset.sdiff_subset_sdiff_right {α : Type u_1} [DecidableEq α] {s t : Finset α} (u : Finset α) (h : s ⊆ t) : u \ t ⊆ u \ s

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

@[simp]

theorem Finset.coe_sdiff {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) : ↑(s₁ \ s₂) = ↑s₁ \ ↑s₂

@[simp]

theorem Finset.union_sdiff_self_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∪ t \ s = s ∪ t

@[simp]

theorem Finset.sdiff_union_self_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} : s \ t ∪ t = s ∪ t

theorem Finset.union_sdiff_left {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t) \ s = t \ s

theorem Finset.union_sdiff_right {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t) \ t = s \ t

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

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

theorem Finset.disjoint_injOn_union_left {α : Type u_1} [DecidableEq α] (s : Finset α) : Set.InjOn (fun (x : Finset α) => x ∪ s) {t : Finset α | Disjoint s t}

· ∪ s is injective on finsets disjoint from s.

theorem Finset.superset_injOn_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) : Set.InjOn (fun (x : Finset α) => x \ s) {t : Finset α | s ⊆ t}

· \ s is injective on finsets containing s.

theorem Finset.union_sdiff_symm {α : Type u_1} [DecidableEq α] {s t : Finset α} : s ∪ t \ s = t ∪ s \ t

theorem Finset.sdiff_union_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : s \ t ∪ s ∩ t = s

theorem Finset.sdiff_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s \ t) \ t = s \ t

theorem Finset.subset_sdiff {α : Type u_1} [DecidableEq α] {s t u : Finset α} : s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u

@[simp]

theorem Finset.sdiff_eq_empty_iff_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} : s \ t = ∅ ↔ s ⊆ t

theorem Finset.sdiff_nonempty {α : Type u_1} [DecidableEq α] {s t : Finset α} : (s \ t).Nonempty ↔ ¬s ⊆ t

@[simp]

theorem Finset.empty_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) : ∅ \ s = ∅

theorem Finset.insert_sdiff_of_notMem {α : Type u_1} [DecidableEq α] (s : Finset α) {t : Finset α} {x : α} (h : x ∉ t) : insert x s \ t = insert x (s \ t)

theorem Finset.insert_sdiff_of_mem {α : Type u_1} [DecidableEq α] {t : Finset α} (s : Finset α) {x : α} (h : x ∈ t) : insert x s \ t = s \ t

@[simp]

theorem Finset.insert_sdiff_self_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) : insert a (s \ {a}) = s

@[simp]

theorem Finset.insert_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∉ s) : insert a s \ s = {a}

@[simp]

theorem Finset.insert_sdiff_insert {α : Type u_1} [DecidableEq α] (s t : Finset α) (x : α) : insert x s \ insert x t = s \ insert x t

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}

theorem Finset.cons_sdiff_cons {α : Type u_1} [DecidableEq α] {s : Finset α} {a b : α} (hab : a ≠ b) (ha : a ∉ s) (hb : b ∉ s) : cons a s ha \ cons b s hb = {a}

theorem Finset.sdiff_insert_of_notMem {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} (h : x ∉ s) (t : Finset α) : s \ insert x t = s \ t

theorem Finset.sdiff_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} : s \ t ⊆ s

theorem Finset.sdiff_ssubset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t ⊆ s) (ht : t.Nonempty) : s \ t ⊂ s

theorem Finset.union_sdiff_distrib {α : Type u_1} [DecidableEq α] (s₁ s₂ t : Finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t

theorem Finset.sdiff_union_distrib {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) : s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)

theorem Finset.union_sdiff_self {α : Type u_1} [DecidableEq α] (s t : Finset α) : (s ∪ t) \ t = s \ t

theorem Finset.Nontrivial.sdiff_singleton_nonempty {α : Type u_1} [DecidableEq α] {c : α} {s : Finset α} (hS : s.Nontrivial) : (s \ {c}).Nonempty

theorem Finset.sdiff_sdiff_left' {α : Type u_1} [DecidableEq α] (s t u : Finset α) : (s \ t) \ u = s \ t ∩ (s \ u)

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

theorem Finset.sdiff_sdiff_eq_sdiff_union {α : Type u_1} [DecidableEq α] {s t u : Finset α} (h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u

theorem Finset.sdiff_sdiff_self_left {α : Type u_1} [DecidableEq α] (s t : Finset α) : s \ (s \ t) = s ∩ t

theorem Finset.sdiff_sdiff_eq_self {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t ⊆ s) : s \ (s \ t) = t

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₂

theorem Finset.union_eq_sdiff_union_sdiff_union_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) : s ∪ t = s \ t ∪ t \ s ∪ s ∩ t

theorem Finset.sdiff_eq_self_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} : s \ t = s ↔ Disjoint s t

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