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

@[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)