mathlib documentation

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

References #

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

https://people.math.gatech.edu/~mccuan/courses/4317/symmetricdifference.pdf

Tags #

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

def symm_diff {α : Type u_1} [has_sup α] [has_sdiff α] (A B : α) :

α

The symmetric difference operator on a type with ⊔ and \ is (A \ B) ⊔ (B \ A).

Equations

A ∆ B = A \ B ⊔ B \ A

theorem symm_diff_def {α : Type u_1} [has_sup α] [has_sdiff α] (A B : α) :

A ∆ B = A \ B ⊔ B \ A

theorem symm_diff_eq_xor (p q : Prop) :

p ∆ q = xor p q

theorem symm_diff_comm {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b = b ∆ a

@[protected, instance]

def symm_diff_is_comm {α : Type u_1} [generalized_boolean_algebra α] :

is_commutative α symm_diff

@[simp]

theorem symm_diff_self {α : Type u_1} [generalized_boolean_algebra α] (a : α) :

@[simp]

theorem symm_diff_bot {α : Type u_1} [generalized_boolean_algebra α] (a : α) :

@[simp]

theorem bot_symm_diff {α : Type u_1} [generalized_boolean_algebra α] (a : α) :

theorem symm_diff_eq_sup_sdiff_inf {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b = (a ⊔ b) \ (a ⊓ b)

@[simp]

theorem sup_sdiff_symm_diff {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

(a ⊔ b) \ a ∆ b = a ⊓ b

theorem disjoint_symm_diff_inf {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

disjoint (a ∆ b) (a ⊓ b)

theorem symm_diff_le_sup {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b ≤ a ⊔ b

theorem inf_symm_diff_distrib_left {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)

theorem inf_symm_diff_distrib_right {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)

theorem sdiff_symm_diff {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b

theorem sdiff_symm_diff' {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)

theorem symm_diff_sdiff {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)

@[simp]

theorem symm_diff_sdiff_left {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b \ a = b \ a

@[simp]

theorem symm_diff_sdiff_right {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b \ b = a \ b

@[simp]

theorem sdiff_symm_diff_self {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a \ a ∆ b = a ⊓ b

theorem symm_diff_eq_iff_sdiff_eq {α : Type u_1} [generalized_boolean_algebra α] {a b c : α} (ha : a ≤ c) :

a ∆ b = c ↔ c \ a = b

theorem disjoint.symm_diff_eq_sup {α : Type u_1} [generalized_boolean_algebra α] {a b : α} (h : disjoint a b) :

a ∆ b = a ⊔ b

theorem symm_diff_eq_sup {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b = a ⊔ b ↔ disjoint a b

theorem symm_diff_symm_diff_left {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b ∆ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

theorem symm_diff_symm_diff_right {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ (b ∆ c) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c

theorem symm_diff_assoc {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b ∆ c = a ∆ (b ∆ c)

@[protected, instance]

def symm_diff_is_assoc {α : Type u_1} [generalized_boolean_algebra α] :

is_associative α symm_diff

theorem symm_diff_left_comm {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ (b ∆ c) = b ∆ (a ∆ c)

theorem symm_diff_right_comm {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b ∆ c = a ∆ c ∆ b

theorem symm_diff_symm_diff_symm_diff_comm {α : Type u_1} [generalized_boolean_algebra α] (a b c d : α) :

a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)

@[simp]

theorem symm_diff_symm_diff_self {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ (a ∆ b) = b

@[simp]

theorem symm_diff_symm_diff_self' {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b ∆ a = b

@[simp]

theorem symm_diff_right_inj {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b = a ∆ c ↔ b = c

@[simp]

theorem symm_diff_left_inj {α : Type u_1} [generalized_boolean_algebra α] (a b c : α) :

a ∆ b = c ∆ b ↔ a = c

@[simp]

theorem symm_diff_eq_left {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b = a ↔ b = ⊥

@[simp]

theorem symm_diff_eq_right {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b = b ↔ a = ⊥

@[simp]

theorem symm_diff_eq_bot {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b = ⊥ ↔ a = b

@[simp]

theorem symm_diff_symm_diff_inf {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

a ∆ b ∆ (a ⊓ b) = a ⊔ b

@[simp]

theorem inf_symm_diff_symm_diff {α : Type u_1} [generalized_boolean_algebra α] (a b : α) :

(a ⊓ b) ∆ (a ∆ b) = a ⊔ b

@[protected]

theorem disjoint.symm_diff_left {α : Type u_1} [generalized_boolean_algebra α] {a b c : α} (ha : disjoint a c) (hb : disjoint b c) :

disjoint (a ∆ b) c

@[protected]

theorem disjoint.symm_diff_right {α : Type u_1} [generalized_boolean_algebra α] {a b c : α} (ha : disjoint a b) (hb : disjoint a c) :

disjoint a (b ∆ c)

theorem symm_diff_eq {α : Type u_1} [boolean_algebra α] (a b : α) :

a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ

@[simp]

theorem symm_diff_top {α : Type u_1} [boolean_algebra α] (a : α) :

a ∆ ⊤ = aᶜ

@[simp]

theorem top_symm_diff {α : Type u_1} [boolean_algebra α] (a : α) :

⊤ ∆ a = aᶜ

theorem compl_symm_diff {α : Type u_1} [boolean_algebra α] (a b : α) :

(a ∆ b)ᶜ = a ⊓ b ⊔ aᶜ ⊓ bᶜ

theorem symm_diff_eq_top_iff {α : Type u_1} [boolean_algebra α] (a b : α) :

a ∆ b = ⊤ ↔ is_compl a b

theorem is_compl.symm_diff_eq_top {α : Type u_1} [boolean_algebra α] (a b : α) (h : is_compl a b) :

@[simp]

theorem compl_symm_diff_self {α : Type u_1} [boolean_algebra α] (a : α) :

aᶜ ∆ a = ⊤

@[simp]

theorem symm_diff_compl_self {α : Type u_1} [boolean_algebra α] (a : α) :

a ∆ aᶜ = ⊤

theorem symm_diff_symm_diff_right' {α : Type u_1} [boolean_algebra α] (a b c : α) :

a ∆ (b ∆ c) = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c