Symmetric difference and bi-implication #
This file defines the symmetric difference and bi-implication operators in (co-)Heyting algebras.
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
- The symmetric difference on
- 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
Main declarations #
symm_diff: 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:
The proof of associativity follows the note "Associativity of the Symmetric Difference of Sets: A
Proof from the Book" by John McCuan:
boolean ring, generalized boolean algebra, boolean algebra, symmetric difference, bi-implication,
The symmetric difference operator on a type with
(A \ B) ⊔ (B \ A).
The Heyting bi-implication is
(b ⇨ a) ⊓ (a ⇨ b). This generalizes equivalence of
- a ⇔ b = (b ⇨ a) ⊓ (a ⇨ b)