Symmetric difference of finite sets

This file concerns the symmetric difference operator s Δ t on finite sets.

Tags

finite sets, finset

Symmetric difference

theorem Finset.mem_symmDiff {α : Type u_1} [DecidableEq α] {s t : Finset α} {a : α} : a ∈ symmDiff s t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

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

@[simp]

theorem Finset.coe_symmDiff {α : Type u_1} [DecidableEq α] {s t : Finset α} : ↑(symmDiff s t) = symmDiff ↑s ↑t

@[simp]

theorem Finset.symmDiff_eq_empty {α : Type u_1} [DecidableEq α] {s t : Finset α} : symmDiff s t = ∅ ↔ s = t

@[simp]

theorem Finset.symmDiff_nonempty {α : Type u_1} [DecidableEq α] {s t : Finset α} : (symmDiff s t).Nonempty ↔ s ≠ t

theorem Finset.image_symmDiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α → β} (s t : Finset α) (hf : Function.Injective f) : image f (symmDiff s t) = symmDiff (image f s) (image f t)

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

See symmDiff_subset_sdiff' for the swapped version of this.

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

See symmDiff_subset_sdiff for the swapped version of this.

theorem Finset.symmDiff_subset_union {α : Type u_1} [DecidableEq α] {s t : Finset α} : symmDiff s t ⊆ s ∪ t

theorem Finset.symmDiff_eq_union_iff {α : Type u_1} [DecidableEq α] (s t : Finset α) : symmDiff s t = s ∪ t ↔ Disjoint s t

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