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