Symmetric difference on finsets and finite types

This module gathers algebraic and combinatorial properties of symmetric difference on finite sets:

• In a generalized Boolean algebra b ↦ a ∆ b is an involution, so over a finite generalized Boolean algebra the product of f (a ∆ b) over all b is the product of f b over all b (Fintype.prod_symmDiff, Fintype.sum_symmDiff).
• Symmetric difference of a finset with a singleton: s ∆ {t} removes t if present and inserts it otherwise (Finset.symmDiff_singleton_eq), bounding the cardinality by s.card + 1 (Finset.card_symmDiff_singleton_le).
• Summing over s ∆ {t} adds val t when elements have order at most 2, in particular in the Boolean ring Bool (Finset.sum_symmDiff_singleton).

Main results

• Fintype.prod_symmDiff, Fintype.sum_symmDiff: reindexing a product or a sum by a symmetric difference.
• Finset.symmDiff_singleton_eq: symmetric difference with a singleton as conditional erase/insert.
• Finset.mem_symmDiff_singleton: membership in s ∆ {t}.
• Finset.card_symmDiff_singleton_le: cardinality bound for s ∆ {t}.
• Finset.sum_symmDiff_singleton: summing over s ∆ {t} adds val t in Bool.

theorem Fintype.prod_symmDiff {α : Type u_1} {M : Type u_2} [Fintype α] [GeneralizedBooleanAlgebra α] [CommMonoid M] (a : α) (f : α → M) : ∏ b : α, f (symmDiff a b) = ∏ b : α, f b

Reindexing a product over a finite generalized Boolean algebra by the involution b ↦ a ∆ b.

theorem Fintype.sum_symmDiff {α : Type u_1} {M : Type u_2} [Fintype α] [GeneralizedBooleanAlgebra α] [AddCommMonoid M] (a : α) (f : α → M) : ∑ b : α, f (symmDiff a b) = ∑ b : α, f b

Reindexing a sum over a finite generalized Boolean algebra by the involution b ↦ a ∆ b.

theorem Finset.symmDiff_singleton_eq {α : Type u_1} [DecidableEq α] (s : Finset α) (t : α) : symmDiff s {t} = if t ∈ s then s.erase t else insert t s

Adding t to a finset by symmetric difference removes it if present and inserts it otherwise.

theorem Finset.mem_symmDiff_singleton {α : Type u_1} [DecidableEq α] {s : Finset α} {t z : α} : z ∈ symmDiff s {t} ↔ (z ∈ s ↔ z ≠ t)

An element belongs to s ∆ {t} if and only if its membership in s differs from equality with t.

theorem Finset.card_symmDiff_singleton_le {α : Type u_1} [DecidableEq α] (s : Finset α) (t : α) : (symmDiff s {t}).card ≤ s.card + 1

The cardinality of s ∆ {t} is at most s.card + 1.

theorem Finset.sum_symmDiff_singleton_of_add_self {α : Type u_1} [DecidableEq α] {M : Type u_2} [AddCommMonoid M] (h_self : ∀ (x : M), x + x = 0) (s : Finset α) (t : α) (val : α → M) : ∑ i ∈ symmDiff s {t}, val i = ∑ i ∈ s, val i + val t

In an additive commutative monoid where every element has order at most 2, summing over s ∆ {t} adds val t.

theorem Finset.sum_symmDiff_singleton {α : Type u_1} [DecidableEq α] (s : Finset α) (t : α) (val : α → Bool) : ∑ i ∈ symmDiff s {t}, val i = ∑ i ∈ s, val i + val t

Summing a Boolean-valued function over s ∆ {t} adds val t in the Boolean ring.