1 files changed, 50 insertions, 0 deletions
diff --git a/library/set/partition.tex b/library/set/partition.tex
new file mode 100644
index 0000000..ed74bf7
--- /dev/null
+++ b/library/set/partition.tex
@@ -0,0 +1,50 @@
+\import{set.tex}
+
+\subsection{Partitions}
+
+\begin{definition}\label{partition}
+    $P$ is a partition iff
+    $\emptyset\notin P$ and
+    for all $B, C\in P$ such that $B\neq C$ we have $B$ is disjoint from $C$.
+\end{definition}
+
+\begin{abbreviation}\label{partition_of}
+    $P$ is a partition of $A$ iff
+    $P$ is a partition and
+    $\unions{P} = A$.
+\end{abbreviation}
+
+\begin{proposition}\label{partition_emptyset}
+    $\emptyset$ is a partition of $\emptyset$.
+\end{proposition}
+
+\begin{definition}\label{partition_refinement}
+    $P'$ is a refinement of $P$ iff
+    for every $A'\in P'$ there exists
+    $A\in P$ such that $A'\subseteq A$.
+\end{definition}
+
+\begin{abbreviation}\label{partition_refines}
+    $P'\refines P$ iff
+    $P'$ is a refinement of $P$.
+\end{abbreviation}
+
+\begin{proposition}\label{partition_refinement_transitive}
+    Suppose $P''\refines P'\refines P$.
+    Then $P''\refines P$.
+\end{proposition}
+\begin{proof}
+    It suffices to show that for all $A''\in P''$ there exists $A\in P$ such that $A''\subseteq A$.
+    Fix $A''\in P''$.
+    Take $A'\in P'$ such that $A''\subseteq A'$
+        by \cref{partition_refinement}.
+    Take $A\in P$ such that $A'\subseteq A$.
+    Then $A''\subseteq A$.
+    Follows by definition. %i.e. A will do for the current existential goal.
+\end{proof}
+
+%\begin{definition}\label{set_of_representatives}
+%    $X$ is a set of representatives for $P$ iff
+%    for all $A\in P$ there exists $a\in A$ such that
+%    $X\inter A = \{a\}$.
+%\end{definition}