Documentation

Mathlib.Data.Finset.SDiff

Difference of finite sets #

Main declarations #

Tags #

finite sets, finset

sdiff #

source
🔸 coverage
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
    source
    📐 coverage
    @[simp]
    theorem Finset.sdiff_val {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
    (s₁ \ s₂).val = s₁.val - s₂.val
    source
    📐 coverage
    @[simp]
    theorem Finset.mem_sdiff {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} :
    a ∈ s \ t ↔ a ∈ s ∧ a ∉ t
    source
    📐 coverage
    @[simp]
    theorem Finset.inter_sdiff_self {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
    s₁ ∩ (s₂ \ s₁) = ∅
    source
    🔸 coverage
    instance Finset.instGeneralizedBooleanAlgebra {α : Type u_1} [DecidableEq α] :
    GeneralizedBooleanAlgebra (Finset α)
    Equations
      source
      📐 coverage
      theorem Finset.notMem_sdiff_of_mem_right {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∈ t) :
      a ∉ s \ t
      source
      📐 coverage
      theorem Finset.notMem_sdiff_of_notMem_left {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} (h : a ∉ s) :
      a ∉ s \ t
      source
      📐 coverage
      theorem Finset.union_sdiff_of_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : s ⊆ t) :
      s ∪ t \ s = t
      source
      📐 coverage
      theorem Finset.sdiff_union_of_subset {α : Type u_1} [DecidableEq α] {s₁ s₂ : Finset α} (h : s₁ ⊆ s₂) :
      s₂ \ s₁ ∪ s₁ = s₂
      source
      📐 coverage
      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.

      source
      📐 coverage
      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.

      source
      📐 coverage
      theorem Finset.inter_sdiff_left_comm {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
      s ∩ (t \ u) = t ∩ (s \ u)
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_inter_self {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
      s₂ \ s₁ ∩ s₁ = ∅
      source
      📐 coverage
      theorem Finset.sdiff_self {α : Type u_1} [DecidableEq α] (s₁ : Finset α) :
      s₁ \ s₁ = ∅
      source
      📐 coverage
      theorem Finset.sdiff_inter_distrib_right {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
      s \ (t ∩ u) = s \ t ∪ s \ u
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_inter_self_left {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      s \ (s ∩ t) = s \ t
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_inter_self_right {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      s \ (t ∩ s) = s \ t
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_empty {α : Type u_1} [DecidableEq α] {s : Finset α} :
      s \ ∅ = s
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      @[simp]
      theorem Finset.coe_sdiff {α : Type u_1} [DecidableEq α] (s₁ s₂ : Finset α) :
      ↑(s₁ \ s₂) = ↑s₁ \ ↑s₂
      source
      📐 coverage
      @[simp]
      theorem Finset.union_sdiff_self_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      s ∪ t \ s = s ∪ t
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_union_self_eq_union {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      s \ t ∪ t = s ∪ t
      source
      📐 coverage
      theorem Finset.union_sdiff_left {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      (s ∪ t) \ s = t \ s
      source
      📐 coverage
      theorem Finset.union_sdiff_right {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      (s ∪ t) \ t = s \ t
      source
      📐 coverage
      theorem Finset.union_sdiff_cancel_left {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) :
      (s ∪ t) \ s = t
      source
      📐 coverage
      theorem Finset.union_sdiff_cancel_right {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) :
      (s ∪ t) \ t = s
      source
      📐 coverage
      theorem Finset.union_sdiff_symm {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      s ∪ t \ s = t ∪ s \ t
      source
      📐 coverage
      theorem Finset.sdiff_union_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      s \ t ∪ s ∩ t = s
      source
      📐 coverage
      theorem Finset.sdiff_idem {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      (s \ t) \ t = s \ t
      source
      📐 coverage
      theorem Finset.subset_sdiff {α : Type u_1} [DecidableEq α] {s t u : Finset α} :
      s ⊆ t \ u ↔ s ⊆ t ∧ Disjoint s u
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_eq_empty_iff_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      s \ t = ∅ ↔ s ⊆ t
      source
      📐 coverage
      theorem Finset.sdiff_nonempty {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      (s \ t).Nonempty ↔ ¬s ⊆ t
      source
      📐 coverage
      @[simp]
      theorem Finset.empty_sdiff {α : Type u_1} [DecidableEq α] (s : Finset α) :
      ∅ \ s = ∅
      source
      📐 coverage
      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)
      source
      📐 coverage
      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
      📐 coverage
      @[simp]
      theorem Finset.insert_sdiff_self_of_mem {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∈ s) :
      insert a (s \ {a}) = s
      source
      📐 coverage
      @[simp]
      theorem Finset.insert_sdiff_cancel {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} (ha : a ∉ s) :
      insert a s \ s = {a}
      source
      📐 coverage
      @[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
      📐 coverage
      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
      📐 coverage
      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}
      source
      📐 coverage
      theorem Finset.sdiff_insert_of_notMem {α : Type u_1} [DecidableEq α] {s : Finset α} {x : α} (h : x ∉ s) (t : Finset α) :
      s \ insert x t = s \ t
      source
      📐 coverage
      @[simp]
      theorem Finset.sdiff_subset {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      s \ t ⊆ s
      source
      📐 coverage
      theorem Finset.sdiff_ssubset {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t ⊆ s) (ht : t.Nonempty) :
      s \ t ⊂ s
      source
      📐 coverage
      theorem Finset.union_sdiff_distrib {α : Type u_1} [DecidableEq α] (s₁ s₂ t : Finset α) :
      (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t
      source
      📐 coverage
      theorem Finset.sdiff_union_distrib {α : Type u_1} [DecidableEq α] (s t₁ t₂ : Finset α) :
      s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂)
      source
      📐 coverage
      theorem Finset.union_sdiff_self {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      (s ∪ t) \ t = s \ t
      source
      📐 coverage
      theorem Finset.Nontrivial.sdiff_singleton_nonempty {α : Type u_1} [DecidableEq α] {c : α} {s : Finset α} (hS : s.Nontrivial) :
      (s \ {c}).Nonempty
      source
      📐 coverage
      theorem Finset.sdiff_sdiff_left' {α : Type u_1} [DecidableEq α] (s t u : Finset α) :
      (s \ t) \ u = s \ t ∩ (s \ u)
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      theorem Finset.sdiff_sdiff_self_left {α : Type u_1} [DecidableEq α] (s t : Finset α) :
      s \ (s \ t) = s ∩ t
      source
      📐 coverage
      theorem Finset.sdiff_sdiff_eq_self {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : t ⊆ s) :
      s \ (s \ t) = t
      source
      📐 coverage
      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
      📐 coverage
      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
      📐 coverage
      theorem Finset.sdiff_eq_self_iff_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} :
      s \ t = s ↔ Disjoint s t
      source
      📐 coverage
      theorem Finset.sdiff_eq_self_of_disjoint {α : Type u_1} [DecidableEq α] {s t : Finset α} (h : Disjoint s t) :
      s \ t = s