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

@[simp]

theorem Set.diff_symmDiff_self {α : Type u_1} (s t : Set α) : s \ symmDiff s t = s ∩ t

@[simp]

theorem Set.symmDiff_diff_self {α : Type u_1} (s t : Set α) : symmDiff s (s \ t) = s ∩ t

@[simp]

theorem Set.inter_union_symmDiff {α : Type u_1} (s t : Set α) : s ∩ t ∪ symmDiff s t = s ∪ t

theorem Set.inter_subset_symmDiff_union_symmDiff {α : Type u_1} {s t u v : Set α} (h : Disjoint u v) : s ∩ t ⊆ symmDiff s u ∪ symmDiff t v

theorem Set.union_symmDiff_of_disjoint {α : Type u_1} {s t u : Set α} (h : Disjoint t u) : symmDiff (s ∪ t) u = symmDiff s u ∪ t

theorem Set.inter_symmDiff_left {α : Type u_1} {s t : Set α} : symmDiff (s ∩ t) s = s \ t

theorem Set.smul_set_def {α : Type u_1} {β : Type u_2} {x : α} {s : Set β} [SMul α β] : x • s = (fun (x_1 : β) => x • x_1) '' s

theorem Set.subset_smul_set {α : Type u_1} {β : Type u_2} {x : α} {s t : Set β} [Group α] [MulAction α β] : t ⊆ x • s ↔ x⁻¹ • t ⊆ s

theorem Set.symmDiff_smul_set {α : Type u_1} {β : Type u_2} {x : α} {s t : Set β} [Group α] [MulAction α β] : x • symmDiff s t = symmDiff (x • s) (x • t)

theorem Set.bounded_lt_union {α : Type u_1} [LinearOrder α] {s t : Set α} (hs : Set.Bounded (fun (x1 x2 : α) => x1 < x2) s) (ht : Set.Bounded (fun (x1 x2 : α) => x1 < x2) t) : Set.Bounded (fun (x1 x2 : α) => x1 < x2) (s ∪ t)