blob: 61f744807482f1454a4ba51455148f60edaf8367 (
plain)
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
|
\subsection{Symmetric difference}
\import{set.tex}
\begin{definition}\label{symdiff}
$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}
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}
Follows by set extensionality.
\end{proof}
\begin{proposition}%
\label{symdiff_comm}
$x\symdiff y = y\symdiff x$.
\end{proposition}
\begin{proof}
Follows by set extensionality.
\end{proof}
|
