Symmetric differences of sets

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

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

@[simp]

theorem Set.mem_bihimp_iff {α : Type u} {a : α} {s t : Set α} : a ∈ bihimp s t ↔ (a ∈ s ↔ a ∈ t)

theorem Set.bihimp_def {α : Type u} {s t : Set α} : bihimp s t = (s ∪ tᶜ) ∩ (t ∪ sᶜ)

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem Set.union_symmDiff_union_subset {α : Type u} {s t u v : Set α} : symmDiff (s ∪ t) (u ∪ v) ⊆ symmDiff s u ∪ symmDiff t v