order.symm_diff

# Symmetric difference #

The symmetric difference or disjunctive union of sets A and B is the set of elements that are in either A or B but not both. Translated into propositions, the symmetric difference is xor.

The symmetric difference operator (symm_diff) is defined in this file for any type with ⊔ and \ via the formula (A \ B) ⊔ (B \ A), however the theorems proved about it only hold for generalized_boolean_algebras and boolean_algebras.

The symmetric difference is the addition operator in the Boolean ring structure on Boolean algebras.

## Main declarations #

• symm_diff: the symmetric difference operator, defined as (A \ B) ⊔ (B \ A)

In generalized Boolean algebras, the symmetric difference operator is:

• symm_diff_comm: commutative, and
• symm_diff_assoc: associative.

## Notations #

• a Δ b: symm_diff a b

The proof of associativity follows the note "Associativity of the Symmetric Difference of Sets: A Proof from the Book" by John McCuan:

## Tags #

boolean ring, generalized boolean algebra, boolean algebra, symmetric differences