Symmetric differences of sets

theorem Set.mem_symmDiff {α : Type u} {a : α} {s : Set α} {t : Set α} : a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

theorem Set.symmDiff_def {α : Type u} (s : Set α) (t : Set α) : symmDiff s t = s \ t ∪ t \ s

theorem Set.symmDiff_subset_union {α : Type u} {s : Set α} {t : Set α} : symmDiff s t ⊆ s ∪ t

@[simp]

theorem Set.symmDiff_eq_empty {α : Type u} {s : Set α} {t : Set α} : symmDiff s t = ∅ ↔ s = t

@[simp]

theorem Set.symmDiff_nonempty {α : Type u} {s : Set α} {t : Set α} : (symmDiff s t).Nonempty ↔ s ≠ t

theorem Set.inter_symmDiff_distrib_left {α : Type u} (s : Set α) (t : Set α) (u : Set α) : s ∩ symmDiff t u = symmDiff (s ∩ t) (s ∩ u)

theorem Set.inter_symmDiff_distrib_right {α : Type u} (s : Set α) (t : Set α) (u : Set α) : symmDiff s t ∩ u = symmDiff (s ∩ u) (t ∩ u)

theorem Set.subset_symmDiff_union_symmDiff_left {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : Disjoint s t) : u ⊆ symmDiff s u ∪ symmDiff t u

theorem Set.subset_symmDiff_union_symmDiff_right {α : Type u} {s : Set α} {t : Set α} {u : Set α} (h : Disjoint t u) : s ⊆ symmDiff s t ∪ symmDiff s u