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 #

In generalized Boolean algebras, the symmetric difference operator is:

Notations #

References #

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

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
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
@[instance]
@[simp]
theorem symm_diff_self {α : Type u_1} [generalized_boolean_algebra α] (a : α) :
a Δ a =
@[simp]
theorem symm_diff_bot {α : Type u_1} [generalized_boolean_algebra α] (a : α) :
a Δ = a
@[simp]
theorem bot_symm_diff {α : Type u_1} [generalized_boolean_algebra α] (a : α) :
Δ a = a
theorem symm_diff_eq_sup_sdiff_inf {α : 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 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)
@[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
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) :
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
theorem disjoint.disjoint_symm_diff_of_disjoint {α : Type u_1} [boolean_algebra α] {a b c : α} (h1 : disjoint a c) (h2 : disjoint b c) :
disjoint (a Δ b) c