# Symmetric difference and bi-implication #

This file defines the symmetric difference and bi-implication operators in (co-)Heyting algebras.

## Examples #

Some examples are

• The symmetric difference of two sets is the set of elements that are in either but not both.
• The symmetric difference on propositions is Xor'.
• The symmetric difference on Bool is Bool.xor.
• The equivalence of propositions. Two propositions are equivalent if they imply each other.
• The symmetric difference translates to addition when considering a Boolean algebra as a Boolean ring.

## Main declarations #

• symmDiff: The symmetric difference operator, defined as (a \ b) ⊔ (b \ a)
• bihimp: The bi-implication operator, defined as (b ⇨ a) ⊓ (a ⇨ b)

In generalized Boolean algebras, the symmetric difference operator is:

• symmDiff_comm: commutative, and
• symmDiff_assoc: associative.

## Notations #

• a ∆ b: symmDiff a b
• a ⇔ b: bihimp 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:

## Tags #

boolean ring, generalized boolean algebra, boolean algebra, symmetric difference, bi-implication, Heyting

def symmDiff {α : Type u_2} [Sup α] [] (a : α) (b : α) :
α

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

Equations
Instances For
def bihimp {α : Type u_2} [Inf α] [HImp α] (a : α) (b : α) :
α

The Heyting bi-implication is (b ⇨ a) ⊓ (a ⇨ b). This generalizes equivalence of propositions.

Equations
Instances For

Notation for symmDiff

Equations
Instances For

Notation for bihimp

Equations
Instances For
theorem symmDiff_def {α : Type u_2} [Sup α] [] (a : α) (b : α) :
symmDiff a b = a \ b b \ a
theorem bihimp_def {α : Type u_2} [Inf α] [HImp α] (a : α) (b : α) :
bihimp a b = (b a) (a b)
theorem symmDiff_eq_Xor' (p : Prop) (q : Prop) :
symmDiff p q = Xor' p q
@[simp]
theorem bihimp_iff_iff {p : Prop} {q : Prop} :
bihimp p q (p q)
@[simp]
theorem Bool.symmDiff_eq_xor (p : Bool) (q : Bool) :
symmDiff p q = xor p q
@[simp]
theorem toDual_symmDiff {α : Type u_2} (a : α) (b : α) :
OrderDual.toDual (symmDiff a b) = bihimp (OrderDual.toDual a) (OrderDual.toDual b)
@[simp]
theorem ofDual_bihimp {α : Type u_2} (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (bihimp a b) = symmDiff (OrderDual.ofDual a) (OrderDual.ofDual b)
theorem symmDiff_comm {α : Type u_2} (a : α) (b : α) :
instance symmDiff_isCommutative {α : Type u_2} :
Std.Commutative fun (x x_1 : α) => symmDiff x x_1
Equations
• =
@[simp]
theorem symmDiff_self {α : Type u_2} (a : α) :
@[simp]
theorem symmDiff_bot {α : Type u_2} (a : α) :
= a
@[simp]
theorem bot_symmDiff {α : Type u_2} (a : α) :
= a
@[simp]
theorem symmDiff_eq_bot {α : Type u_2} {a : α} {b : α} :
symmDiff a b = a = b
theorem symmDiff_of_le {α : Type u_2} {a : α} {b : α} (h : a b) :
symmDiff a b = b \ a
theorem symmDiff_of_ge {α : Type u_2} {a : α} {b : α} (h : b a) :
symmDiff a b = a \ b
theorem symmDiff_le {α : Type u_2} {a : α} {b : α} {c : α} (ha : a b c) (hb : b a c) :
theorem symmDiff_le_iff {α : Type u_2} {a : α} {b : α} {c : α} :
symmDiff a b c a b c b a c
@[simp]
theorem symmDiff_le_sup {α : Type u_2} {a : α} {b : α} :
symmDiff a b a b
theorem symmDiff_eq_sup_sdiff_inf {α : Type u_2} (a : α) (b : α) :
symmDiff a b = (a b) \ (a b)
theorem Disjoint.symmDiff_eq_sup {α : Type u_2} {a : α} {b : α} (h : Disjoint a b) :
symmDiff a b = a b
theorem symmDiff_sdiff {α : Type u_2} (a : α) (b : α) (c : α) :
symmDiff a b \ c = a \ (b c) b \ (a c)
@[simp]
theorem symmDiff_sdiff_inf {α : Type u_2} (a : α) (b : α) :
symmDiff a b \ (a b) = symmDiff a b
@[simp]
theorem symmDiff_sdiff_eq_sup {α : Type u_2} (a : α) (b : α) :
symmDiff a (b \ a) = a b
@[simp]
theorem sdiff_symmDiff_eq_sup {α : Type u_2} (a : α) (b : α) :
symmDiff (a \ b) b = a b
@[simp]
theorem symmDiff_sup_inf {α : Type u_2} (a : α) (b : α) :
symmDiff a b a b = a b
@[simp]
theorem inf_sup_symmDiff {α : Type u_2} (a : α) (b : α) :
a b symmDiff a b = a b
@[simp]
theorem symmDiff_symmDiff_inf {α : Type u_2} (a : α) (b : α) :
symmDiff (symmDiff a b) (a b) = a b
@[simp]
theorem inf_symmDiff_symmDiff {α : Type u_2} (a : α) (b : α) :
symmDiff (a b) (symmDiff a b) = a b
theorem symmDiff_triangle {α : Type u_2} (a : α) (b : α) (c : α) :
theorem le_symmDiff_sup_right {α : Type u_2} (a : α) (b : α) :
a symmDiff a b b
theorem le_symmDiff_sup_left {α : Type u_2} (a : α) (b : α) :
b symmDiff a b a
@[simp]
theorem toDual_bihimp {α : Type u_2} (a : α) (b : α) :
OrderDual.toDual (bihimp a b) = symmDiff (OrderDual.toDual a) (OrderDual.toDual b)
@[simp]
theorem ofDual_symmDiff {α : Type u_2} (a : αᵒᵈ) (b : αᵒᵈ) :
OrderDual.ofDual (symmDiff a b) = bihimp (OrderDual.ofDual a) (OrderDual.ofDual b)
theorem bihimp_comm {α : Type u_2} (a : α) (b : α) :
bihimp a b = bihimp b a
instance bihimp_isCommutative {α : Type u_2} :
Std.Commutative fun (x x_1 : α) => bihimp x x_1
Equations
• =
@[simp]
theorem bihimp_self {α : Type u_2} (a : α) :
@[simp]
theorem bihimp_top {α : Type u_2} (a : α) :
= a
@[simp]
theorem top_bihimp {α : Type u_2} (a : α) :
= a
@[simp]
theorem bihimp_eq_top {α : Type u_2} {a : α} {b : α} :
bihimp a b = a = b
theorem bihimp_of_le {α : Type u_2} {a : α} {b : α} (h : a b) :
bihimp a b = b a
theorem bihimp_of_ge {α : Type u_2} {a : α} {b : α} (h : b a) :
bihimp a b = a b
theorem le_bihimp {α : Type u_2} {a : α} {b : α} {c : α} (hb : a b c) (hc : a c b) :
a bihimp b c
theorem le_bihimp_iff {α : Type u_2} {a : α} {b : α} {c : α} :
a bihimp b c a b c a c b
@[simp]
theorem inf_le_bihimp {α : Type u_2} {a : α} {b : α} :
a b bihimp a b
theorem bihimp_eq_inf_himp_inf {α : Type u_2} (a : α) (b : α) :
bihimp a b = a b a b
theorem Codisjoint.bihimp_eq_inf {α : Type u_2} {a : α} {b : α} (h : ) :
bihimp a b = a b
theorem himp_bihimp {α : Type u_2} (a : α) (b : α) (c : α) :
a bihimp b c = (a c b) (a b c)
@[simp]
theorem sup_himp_bihimp {α : Type u_2} (a : α) (b : α) :
a b bihimp a b = bihimp a b
@[simp]
theorem bihimp_himp_eq_inf {α : Type u_2} (a : α) (b : α) :
bihimp a (a b) = a b
@[simp]
theorem himp_bihimp_eq_inf {α : Type u_2} (a : α) (b : α) :
bihimp (b a) b = a b
@[simp]
theorem bihimp_inf_sup {α : Type u_2} (a : α) (b : α) :
bihimp a b (a b) = a b
@[simp]
theorem sup_inf_bihimp {α : Type u_2} (a : α) (b : α) :
(a b) bihimp a b = a b
@[simp]
theorem bihimp_bihimp_sup {α : Type u_2} (a : α) (b : α) :
bihimp (bihimp a b) (a b) = a b
@[simp]
theorem sup_bihimp_bihimp {α : Type u_2} (a : α) (b : α) :
bihimp (a b) (bihimp a b) = a b
theorem bihimp_triangle {α : Type u_2} (a : α) (b : α) (c : α) :
bihimp a b bihimp b c bihimp a c
@[simp]
theorem symmDiff_top' {α : Type u_2} [] (a : α) :
= a
@[simp]
theorem top_symmDiff' {α : Type u_2} [] (a : α) :
= a
@[simp]
theorem hnot_symmDiff_self {α : Type u_2} [] (a : α) :
@[simp]
theorem symmDiff_hnot_self {α : Type u_2} [] (a : α) :
theorem IsCompl.symmDiff_eq_top {α : Type u_2} [] {a : α} {b : α} (h : IsCompl a b) :
@[simp]
theorem bihimp_bot {α : Type u_2} [] (a : α) :
= a
@[simp]
theorem bot_bihimp {α : Type u_2} [] (a : α) :
= a
@[simp]
theorem compl_bihimp_self {α : Type u_2} [] (a : α) :
@[simp]
theorem bihimp_hnot_self {α : Type u_2} [] (a : α) :
theorem IsCompl.bihimp_eq_bot {α : Type u_2} [] {a : α} {b : α} (h : IsCompl a b) :
@[simp]
theorem sup_sdiff_symmDiff {α : Type u_2} (a : α) (b : α) :
(a b) \ symmDiff a b = a b
theorem disjoint_symmDiff_inf {α : Type u_2} (a : α) (b : α) :
Disjoint (symmDiff a b) (a b)
theorem inf_symmDiff_distrib_left {α : Type u_2} (a : α) (b : α) (c : α) :
a symmDiff b c = symmDiff (a b) (a c)
theorem inf_symmDiff_distrib_right {α : Type u_2} (a : α) (b : α) (c : α) :
symmDiff a b c = symmDiff (a c) (b c)
theorem sdiff_symmDiff {α : Type u_2} (a : α) (b : α) (c : α) :
c \ symmDiff a b = c a b c \ a c \ b
theorem sdiff_symmDiff' {α : Type u_2} (a : α) (b : α) (c : α) :
c \ symmDiff a b = c a b c \ (a b)
@[simp]
theorem symmDiff_sdiff_left {α : Type u_2} (a : α) (b : α) :
symmDiff a b \ a = b \ a
@[simp]
theorem symmDiff_sdiff_right {α : Type u_2} (a : α) (b : α) :
symmDiff a b \ b = a \ b
@[simp]
theorem sdiff_symmDiff_left {α : Type u_2} (a : α) (b : α) :
a \ symmDiff a b = a b
@[simp]
theorem sdiff_symmDiff_right {α : Type u_2} (a : α) (b : α) :
b \ symmDiff a b = a b
theorem symmDiff_eq_sup {α : Type u_2} (a : α) (b : α) :
symmDiff a b = a b Disjoint a b
@[simp]
theorem le_symmDiff_iff_left {α : Type u_2} (a : α) (b : α) :
@[simp]
theorem le_symmDiff_iff_right {α : Type u_2} (a : α) (b : α) :
theorem symmDiff_symmDiff_left {α : Type u_2} (a : α) (b : α) (c : α) :
symmDiff (symmDiff a b) c = a \ (b c) b \ (a c) c \ (a b) a b c
theorem symmDiff_symmDiff_right {α : Type u_2} (a : α) (b : α) (c : α) :
symmDiff a (symmDiff b c) = a \ (b c) b \ (a c) c \ (a b) a b c
theorem symmDiff_assoc {α : Type u_2} (a : α) (b : α) (c : α) :
instance symmDiff_isAssociative {α : Type u_2} :
Std.Associative fun (x x_1 : α) => symmDiff x x_1
Equations
• =
theorem symmDiff_left_comm {α : Type u_2} (a : α) (b : α) (c : α) :
theorem symmDiff_right_comm {α : Type u_2} (a : α) (b : α) (c : α) :
theorem symmDiff_symmDiff_symmDiff_comm {α : Type u_2} (a : α) (b : α) (c : α) (d : α) :
@[simp]
theorem symmDiff_symmDiff_cancel_left {α : Type u_2} (a : α) (b : α) :
symmDiff a (symmDiff a b) = b
@[simp]
theorem symmDiff_symmDiff_cancel_right {α : Type u_2} (a : α) (b : α) :
symmDiff (symmDiff b a) a = b
@[simp]
theorem symmDiff_symmDiff_self' {α : Type u_2} (a : α) (b : α) :
symmDiff (symmDiff a b) a = b
theorem symmDiff_left_involutive {α : Type u_2} (a : α) :
Function.Involutive fun (x : α) => symmDiff x a
theorem symmDiff_right_involutive {α : Type u_2} (a : α) :
Function.Involutive fun (x : α) => symmDiff a x
theorem symmDiff_left_injective {α : Type u_2} (a : α) :
Function.Injective fun (x : α) => symmDiff x a
theorem symmDiff_right_injective {α : Type u_2} (a : α) :
Function.Injective fun (x : α) => symmDiff a x
theorem symmDiff_left_surjective {α : Type u_2} (a : α) :
Function.Surjective fun (x : α) => symmDiff x a
theorem symmDiff_right_surjective {α : Type u_2} (a : α) :
Function.Surjective fun (x : α) => symmDiff a x
@[simp]
theorem symmDiff_left_inj {α : Type u_2} {a : α} {b : α} {c : α} :
symmDiff a b = symmDiff c b a = c
@[simp]
theorem symmDiff_right_inj {α : Type u_2} {a : α} {b : α} {c : α} :
symmDiff a b = symmDiff a c b = c
@[simp]
theorem symmDiff_eq_left {α : Type u_2} {a : α} {b : α} :
symmDiff a b = a b =
@[simp]
theorem symmDiff_eq_right {α : Type u_2} {a : α} {b : α} :
symmDiff a b = b a =
theorem Disjoint.symmDiff_left {α : Type u_2} {a : α} {b : α} {c : α} (ha : Disjoint a c) (hb : Disjoint b c) :
theorem Disjoint.symmDiff_right {α : Type u_2} {a : α} {b : α} {c : α} (ha : Disjoint a b) (hb : Disjoint a c) :
theorem symmDiff_eq_iff_sdiff_eq {α : Type u_2} {a : α} {b : α} {c : α} (ha : a c) :
symmDiff a b = c c \ a = b

CogeneralizedBooleanAlgebra isn't actually a typeclass, but the lemmas in here are dual to the GeneralizedBooleanAlgebra ones

@[simp]
theorem inf_himp_bihimp {α : Type u_2} [] (a : α) (b : α) :
bihimp a b a b = a b
theorem codisjoint_bihimp_sup {α : Type u_2} [] (a : α) (b : α) :
Codisjoint (bihimp a b) (a b)
@[simp]
theorem himp_bihimp_left {α : Type u_2} [] (a : α) (b : α) :
a bihimp a b = a b
@[simp]
theorem himp_bihimp_right {α : Type u_2} [] (a : α) (b : α) :
b bihimp a b = b a
@[simp]
theorem bihimp_himp_left {α : Type u_2} [] (a : α) (b : α) :
bihimp a b a = a b
@[simp]
theorem bihimp_himp_right {α : Type u_2} [] (a : α) (b : α) :
bihimp a b b = a b
@[simp]
theorem bihimp_eq_inf {α : Type u_2} [] (a : α) (b : α) :
bihimp a b = a b
@[simp]
theorem bihimp_le_iff_left {α : Type u_2} [] (a : α) (b : α) :
bihimp a b a
@[simp]
theorem bihimp_le_iff_right {α : Type u_2} [] (a : α) (b : α) :
bihimp a b b
theorem bihimp_assoc {α : Type u_2} [] (a : α) (b : α) (c : α) :
bihimp (bihimp a b) c = bihimp a (bihimp b c)
instance bihimp_isAssociative {α : Type u_2} [] :
Std.Associative fun (x x_1 : α) => bihimp x x_1
Equations
• =
theorem bihimp_left_comm {α : Type u_2} [] (a : α) (b : α) (c : α) :
bihimp a (bihimp b c) = bihimp b (bihimp a c)
theorem bihimp_right_comm {α : Type u_2} [] (a : α) (b : α) (c : α) :
bihimp (bihimp a b) c = bihimp (bihimp a c) b
theorem bihimp_bihimp_bihimp_comm {α : Type u_2} [] (a : α) (b : α) (c : α) (d : α) :
bihimp (bihimp a b) (bihimp c d) = bihimp (bihimp a c) (bihimp b d)
@[simp]
theorem bihimp_bihimp_cancel_left {α : Type u_2} [] (a : α) (b : α) :
bihimp a (bihimp a b) = b
@[simp]
theorem bihimp_bihimp_cancel_right {α : Type u_2} [] (a : α) (b : α) :
bihimp (bihimp b a) a = b
@[simp]
theorem bihimp_bihimp_self {α : Type u_2} [] (a : α) (b : α) :
bihimp (bihimp a b) a = b
theorem bihimp_left_involutive {α : Type u_2} [] (a : α) :
Function.Involutive fun (x : α) => bihimp x a
theorem bihimp_right_involutive {α : Type u_2} [] (a : α) :
Function.Involutive fun (x : α) => bihimp a x
theorem bihimp_left_injective {α : Type u_2} [] (a : α) :
Function.Injective fun (x : α) => bihimp x a
theorem bihimp_right_injective {α : Type u_2} [] (a : α) :
Function.Injective fun (x : α) => bihimp a x
theorem bihimp_left_surjective {α : Type u_2} [] (a : α) :
Function.Surjective fun (x : α) => bihimp x a
theorem bihimp_right_surjective {α : Type u_2} [] (a : α) :
Function.Surjective fun (x : α) => bihimp a x
@[simp]
theorem bihimp_left_inj {α : Type u_2} [] {a : α} {b : α} {c : α} :
bihimp a b = bihimp c b a = c
@[simp]
theorem bihimp_right_inj {α : Type u_2} [] {a : α} {b : α} {c : α} :
bihimp a b = bihimp a c b = c
@[simp]
theorem bihimp_eq_left {α : Type u_2} [] {a : α} {b : α} :
bihimp a b = a b =
@[simp]
theorem bihimp_eq_right {α : Type u_2} [] {a : α} {b : α} :
bihimp a b = b a =
theorem Codisjoint.bihimp_left {α : Type u_2} [] {a : α} {b : α} {c : α} (ha : ) (hb : ) :
theorem Codisjoint.bihimp_right {α : Type u_2} [] {a : α} {b : α} {c : α} (ha : ) (hb : ) :
theorem symmDiff_eq {α : Type u_2} [] (a : α) (b : α) :
symmDiff a b = a b b a
theorem bihimp_eq {α : Type u_2} [] (a : α) (b : α) :
bihimp a b = (a b) (b a)
theorem symmDiff_eq' {α : Type u_2} [] (a : α) (b : α) :
symmDiff a b = (a b) (a b)
theorem bihimp_eq' {α : Type u_2} [] (a : α) (b : α) :
bihimp a b = a b a b
theorem symmDiff_top {α : Type u_2} [] (a : α) :
= a
theorem top_symmDiff {α : Type u_2} [] (a : α) :
= a
@[simp]
theorem compl_symmDiff {α : Type u_2} [] (a : α) (b : α) :
(symmDiff a b) = bihimp a b
@[simp]
theorem compl_bihimp {α : Type u_2} [] (a : α) (b : α) :
(bihimp a b) = symmDiff a b
@[simp]
theorem compl_symmDiff_compl {α : Type u_2} [] (a : α) (b : α) :
= symmDiff a b
@[simp]
theorem compl_bihimp_compl {α : Type u_2} [] (a : α) (b : α) :
@[simp]
theorem symmDiff_eq_top {α : Type u_2} [] (a : α) (b : α) :
@[simp]
theorem bihimp_eq_bot {α : Type u_2} [] (a : α) (b : α) :
@[simp]
theorem compl_symmDiff_self {α : Type u_2} [] (a : α) :
@[simp]
theorem symmDiff_compl_self {α : Type u_2} [] (a : α) :
theorem symmDiff_symmDiff_right' {α : Type u_2} [] (a : α) (b : α) (c : α) :
theorem Disjoint.le_symmDiff_sup_symmDiff_left {α : Type u_2} [] {a : α} {b : α} {c : α} (h : Disjoint a b) :
theorem Disjoint.le_symmDiff_sup_symmDiff_right {α : Type u_2} [] {a : α} {b : α} {c : α} (h : Disjoint b c) :
theorem Codisjoint.bihimp_inf_bihimp_le_left {α : Type u_2} [] {a : α} {b : α} {c : α} (h : ) :
bihimp a c bihimp b c c
theorem Codisjoint.bihimp_inf_bihimp_le_right {α : Type u_2} [] {a : α} {b : α} {c : α} (h : ) :
bihimp a b bihimp a c a

### Prod #

@[simp]
theorem symmDiff_fst {α : Type u_2} {β : Type u_3} (a : α × β) (b : α × β) :
(symmDiff a b).1 = symmDiff a.1 b.1
@[simp]
theorem symmDiff_snd {α : Type u_2} {β : Type u_3} (a : α × β) (b : α × β) :
(symmDiff a b).2 = symmDiff a.2 b.2
@[simp]
theorem bihimp_fst {α : Type u_2} {β : Type u_3} (a : α × β) (b : α × β) :
(bihimp a b).1 = bihimp a.1 b.1
@[simp]
theorem bihimp_snd {α : Type u_2} {β : Type u_3} (a : α × β) (b : α × β) :
(bihimp a b).2 = bihimp a.2 b.2

### Pi #

theorem Pi.symmDiff_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → ] (a : (i : ι) → π i) (b : (i : ι) → π i) :
symmDiff a b = fun (i : ι) => symmDiff (a i) (b i)
theorem Pi.bihimp_def {ι : Type u_1} {π : ιType u_4} [(i : ι) → ] (a : (i : ι) → π i) (b : (i : ι) → π i) :
bihimp a b = fun (i : ι) => bihimp (a i) (b i)
@[simp]
theorem Pi.symmDiff_apply {ι : Type u_1} {π : ιType u_4} [(i : ι) → ] (a : (i : ι) → π i) (b : (i : ι) → π i) (i : ι) :
symmDiff a b i = symmDiff (a i) (b i)
@[simp]
theorem Pi.bihimp_apply {ι : Type u_1} {π : ιType u_4} [(i : ι) → ] (a : (i : ι) → π i) (b : (i : ι) → π i) (i : ι) :
bihimp a b i = bihimp (a i) (b i)