From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 10 Feb 2024 02:22:14 +0100
Subject: Initial commit

---
 library/set/symdiff.tex | 45 +++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 45 insertions(+)
 create mode 100644 library/set/symdiff.tex

(limited to 'library/set/symdiff.tex')

diff --git a/library/set/symdiff.tex b/library/set/symdiff.tex
new file mode 100644
index 0000000..61f7448
--- /dev/null
+++ b/library/set/symdiff.tex
@@ -0,0 +1,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}
-- 
cgit v1.2.3