1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
\subsection{Symmetric difference}
\import{set.tex}
\begin{definition}\label{symdiff}
%! infixl 1
$x\symdiff y = (x\setminus y)\union (y\setminus x)$.
\end{definition}
\begin{proposition}%
\label{symdiff_as_setdiff}
$x\symdiff y = (x\union y)\setminus (y\inter x)$.
\end{proposition}
\begin{proof}
We have for all $z\in x\symdiff y$
we have $z\in (x\union y)\setminus (y\inter x)$
by \cref{inter,setminus,symdiff,union}.
We have for all $z\in (x\union y)\setminus (y\inter x)$
we have $z\in x\symdiff y$
by \cref{inter,setminus,symdiff,union}.
Follows by set extensionality.
\end{proof}
\begin{proposition}%
\label{symdiff_implies_xor_in}
If $z\in x\symdiff y$, then either $z\in x$ or $z\in y$.
\end{proposition}
\begin{proposition}%
\label{xor_in_implies_symdiff}
If either $z\in x$ or $z\in y$, then $z\in x\symdiff y$.
\end{proposition}
\begin{proof}
If $z\in x$ and $z\not\in y$, then $z\in x\setminus y$.
If $z\not\in x$ and $z\in y$, then $z\in y\setminus x$.
\end{proof}
\begin{proposition}%
\label{symdiff_assoc}
$x\symdiff (y\symdiff z) = (x\symdiff y)\symdiff z$.
\end{proposition}
\begin{proof}
We have for all $a\in x\symdiff (y\symdiff z)$
we have $a\in (x\symdiff y)\symdiff z$
by \cref{setminus,symdiff,union}.
We have for all $a\in (x\symdiff y)\symdiff z$
we have $a\in x\symdiff (y\symdiff z)$
by \cref{setminus,symdiff,union}.
Follows by set extensionality.
\end{proof}
\begin{proposition}%
\label{symdiff_comm}
$x\symdiff y = y\symdiff x$.
\end{proposition}
\begin{proof}
We have for all $z\in x\symdiff y$
we have $z\in y\symdiff x$
by \cref{setminus,symdiff,union}.
We have for all $z\in y\symdiff x$
we have $z\in x\symdiff y$
by \cref{setminus,symdiff,union}.
Follows by set extensionality.
\end{proof}
|
