Initial commit

12 files changed, 875 insertions, 0 deletions

diff --git a/library/set/bipartition.tex b/library/set/bipartition.tex
new file mode 100644
index 0000000..e6a76dc
--- /dev/null
+++ b/library/set/bipartition.tex
@@ -0,0 +1,72 @@
+% The theory of splitting sets into two (inhabited, disjoint) partitions.
+
+% See also "bisections" here: https://isarmathlib.org/Partitions_ZF.html
+
+\import{set.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+
+\subsection{Bipartitions}
+
+\begin{abbreviation}\label{bipartitions}
+    $C$ is partitioned by $A$ and $B$ iff $A,B\neq\emptyset$ and $A$ is disjoint from $B$ and $A\union B = C$.
+\end{abbreviation}
+
+\begin{definition}\label{bipartitions_of_a_set}
+    $\bipartitions{X} = \{ p\in\pow{X}\times\pow{X}\mid \text{$X$ is partitioned by $\fst{p}$ and $\snd{p}$}\}$.
+\end{definition}
+
+\begin{abbreviation}\label{is_a_bipartition_of}
+    $P$ is a bipartition of $X$ iff $P\in\bipartitions{X}$.
+\end{abbreviation}
+
+\begin{proposition}\label{bipartition_intro}
+    Suppose $C$ is partitioned by $A$ and $B$.
+    Then $(A, B)$ is a bipartition of $C$.
+\end{proposition}
+\begin{proof}
+    $(A,B)\in\pow{C}\times\pow{C}$.
+    $C$ is partitioned by $\fst{(A,B)}$ and $\snd{(A,B)}$.
+    Thus $(A, B)$ is a bipartition of $C$ by \cref{bipartitions_of_a_set}.
+\end{proof}
+
+\begin{proposition}\label{bipartition_elim}
+    Suppose $(A, B)$ is a bipartition of $C$.
+    Then $C$ is partitioned by $A$ and $B$.
+\end{proposition}
+\begin{proof}
+    $\fst{(A, B)} = A$.
+    $\snd{(A, B)} = B$.
+\end{proof}
+
+\begin{proposition}\label{bipartitions_emptyset}
+    $\bipartitions{\emptyset}$ is empty.
+\end{proposition}
+
+\begin{proposition}\label{union_eq_cons_implies_union_remove_eq}
+    Suppose $d\notin C$.
+    Suppose $A\union B = \cons{d}{C}$.
+    Suppose $A, B\neq \{d\}$.
+    Then $\remove{d}{A}\union \remove{d}{B} = C$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{bipartitions_cons}
+    Suppose $d\notin C$.
+    Suppose $\cons{d}{C}$ is partitioned by $A$ and $B$.
+    Suppose $A, B\neq \{d\}$.
+    Then $C$ is partitioned by $\remove{d}{A}$ and $\remove{d}{B}$.
+\end{proposition}
+\begin{proof}
+    $\remove{d}{A},\remove{d}{B}\neq\emptyset$.
+    $\remove{d}{A}\union \remove{d}{B} = C$ by \cref{union_eq_cons_implies_union_remove_eq}.
+\end{proof}
+
+% TODO
+%\begin{proposition}\label{singleton_bipartition}
+%    Suppose $b\notin A$.
+%    Suppose $A$ and $\{b\}$ bipartition $\cons{b}{C}$.
+%    Then $A = C$.
+%\end{proposition}
diff --git a/library/set/cantor.tex b/library/set/cantor.tex
new file mode 100644
index 0000000..f7c4b2b
--- /dev/null
+++ b/library/set/cantor.tex
@@ -0,0 +1,18 @@
+\import{set/powerset.tex}
+\import{function.tex}
+
+\subsection{Cantor's theorem}
+
+
+\begin{theorem}[Cantor]\label{cantor}
+    There exists no surjection from $A$ to $\pow{A}$.
+\end{theorem}
+\begin{proof}
+    Suppose not.
+    Consider a surjection $f$ from $A$ to $\pow{A}$.
+    Let $B = \{a \in A \mid a\notin f(a)\}$.
+    Then $B\in\pow{A}$.
+    There exists $a'\in A$ such that $f(a') = B$ by \hyperref[surj]{the definition of surjectivity}.
+    Now $a' \in B$ iff $a' \notin f(a') = B$.
+    Contradiction.
+\end{proof}
diff --git a/library/set/cons.tex b/library/set/cons.tex
new file mode 100644
index 0000000..e03ba4f
--- /dev/null
+++ b/library/set/cons.tex
@@ -0,0 +1,112 @@
+\import{set.tex}
+
+\subsection{Additional results about cons}
+
+\begin{proposition}\label{cons_subseteq_intro}
+    Suppose $x\in X$.
+    Suppose $Y\subseteq X$.
+    Then $\cons{x}{Y}\subseteq X$.
+\end{proposition}
+
+\begin{proposition}\label{cons_subseteq_elim}
+    Suppose $\cons{x}{Y}\subseteq X$.
+    Then $x\in X$ and $Y\subseteq X$.
+\end{proposition}
+
+\begin{proposition}\label{cons_subseteq_iff}
+    $\cons{x}{Y}\subseteq X$ iff $x\in X$ and $Y\subseteq X$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_cons_right}
+    If $C\subseteq B$, then $C\subseteq \cons{a}{B}$.
+\end{proposition}
+
+\begin{corollary}\label{subseteq_cons_self}
+    $X\subseteq \cons{y}{X}$.
+\end{corollary}
+
+\begin{abbreviation}\label{remove_point}
+    $\remove{a}{B} = B\setminus\{a\}$.
+\end{abbreviation}
+
+\begin{proposition}\label{subseteq_cons_intro_left}
+    Suppose $a\in C \land \remove{a}{C} \subseteq B$.
+    Then $C\subseteq \cons{a}{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{setminus_cons,setminus_eq_emptyset_iff_subseteq}.
+\end{proof}
+
+\begin{proposition}\label{subseteq_cons_intro_right}
+    Suppose $C \subseteq B$.
+    Then $C\subseteq \cons{a}{B}$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_cons_elim}
+    Suppose $C\subseteq \cons{a}{B}$.
+    Then $C\subseteq B \lor (a\in C \land \remove{a}{C} \subseteq B)$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{setminus_cons,subseteq,cons_iff,setminus_eq_emptyset_iff_subseteq}.
+\end{proof}
+
+\begin{proposition}\label{subseteq_cons_iff}
+    $C\subseteq \cons{a}{B}$ iff $C\subseteq B \lor (a\in C \land \remove{a}{C}\subseteq B)$.
+\end{proposition}
+
+
+\begin{proposition}\label{remove_point_eq_setminus_singleton}
+    $\remove{a}{B} = B\setminus\{a\}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+
+\begin{proposition}\label{union_eq_cons}
+    $\{a\}\union B = \cons{a}{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_comm}
+    $\cons{a}{\cons{b}{C}} = \cons{b}{\cons{a}{C}}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_absorb}
+    Suppose $a\in A$.
+    Then $\cons{a}{A} = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_remove}
+    Suppose $a\in A$.
+    Then $\cons{a}{A\setminus\{a\}} = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{cons_idempotent}
+    Then $\cons{a}{\cons{a}{B}} = \cons{a}{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inters_cons}
+    Suppose $B$ is inhabited.
+    Then $\inters{\cons{a}{B}} = a\inter\inters{B}$.
+\end{proposition}
+\begin{proof}
+    $\cons{a}{B}$ is inhabited.
+    Thus for all $c$ we have $c\in\inters{\cons{a}{B}}$ iff $c\in a\inter \inters{B}$
+        by \cref{inters_iff_forall,cons_iff,inter}.
+    Follows by \hyperref[setext]{extensionality}.
+\end{proof}
diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex
new file mode 100644
index 0000000..a846b78
--- /dev/null
+++ b/library/set/equinumerosity.tex
@@ -0,0 +1,68 @@
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{function.tex}
+
+
+\begin{definition}\label{equinum}
+    $A$ is equinumerous with $B$ iff there exists a bijection from $A$ to $B$.
+\end{definition}
+
+\begin{abbreviation}\label{approx}
+    $A\approx B$ iff $A$ is equinumerous with $B$.
+\end{abbreviation}
+
+\begin{proposition}\label{equinum_refl}
+    $A\approx A$.
+\end{proposition}
+\begin{proof}
+    $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}.
+    Follows by \cref{equinum}.
+\end{proof}
+
+\begin{proposition}\label{equinum_sym}
+    Suppose $A\approx B$. Then $B\approx A$.
+\end{proposition}
+\begin{proof}
+    Take a bijection $f$ from $A$ to $B$ by \cref{equinum}.
+    Then $\converse{f}$ is a bijection from $B$ to $A$ by \cref{bijection_converse_is_bijection}.
+    Follows by \cref{equinum}.
+\end{proof}
+
+\begin{proposition}\label{equinum_tran}
+    Suppose $A\approx B\approx C$. Then $A\approx C$.
+\end{proposition}
+\begin{proof}
+    Take a bijection $f$ from $A$ to $B$ by \cref{equinum}.
+    Take a bijection $g$ from $B$ to $C$ by \cref{equinum}.
+    Then $g\circ f$ is a bijection from $A$ to $C$ by \cref{bijection_circ}.
+    Follows by \cref{equinum}.
+\end{proof}
+
+
+
+\begin{theorem}[Cantor--Schröder--Bernstein]\label{cantorschroederbernstein}
+    Let $f$ be an injective function from $A$ to $B$.
+    Let $g$ be an injective function from $B$ to $A$.
+    Then $A\approx B$.
+\end{theorem}
+\begin{proof}
+    Let $h(X) = A\setminus \img{g}{B\setminus\img{f}{X}}$ for $X\in\pow{A}$.
+    %By construction: $h$ is a relation.
+    %By construction: $h$ is right-unique.
+    %By construction: $\dom{h} = \pow{A}$.
+    For all $X\in\pow{A}$ we have $h(X)\in\pow{A}$ by \cref{setminus_subseteq,pow_iff}.
+    Thus $h$ is a function from $\pow{A}$ to $\pow{A}$.
+
+    $h$ is \subseteq-preserving by \cref{subseteqpreserving,img_subseteq,subseteq_implies_setminus_supseteq}. % apply each each lemma twice (alternating).
+
+    Take a fixpoint $X$ of $h$ by \cref{knastertarski}.
+    Now $X = A\setminus \img{g}{B\setminus\img{f}{X}}$ by \cref{fixpoint}.
+
+    $\img{g}{B\setminus\img{f}{X}}\subseteq A$.
+
+    Thus $\img{g}{B\setminus\img{f}{X}} = A\setminus X$ by \cref{double_relative_complement}.
+
+    Let $h' = \restrl{h}{X}$.
+
+    Omitted. % TODO
+\end{proof}
diff --git a/library/set/filter.tex b/library/set/filter.tex
new file mode 100644
index 0000000..2797d86
--- /dev/null
+++ b/library/set/filter.tex
@@ -0,0 +1,97 @@
+\import{set.tex}
+\import{set/powerset.tex}
+
+\section{Filters}
+
+\begin{abbreviation}\label{upwardclosed}
+    $F$ is upward-closed in $S$ iff
+    for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$.
+\end{abbreviation}
+
+\begin{definition}\label{filter}
+    $F$ is a filter on $S$ iff
+    $F$ is a family of subsets of $S$
+    and $S$ is inhabited
+    and $S\in F$
+    and $\emptyset\notin F$
+    and $F$ is closed under binary intersections
+    and $F$ is upward-closed in $S$.
+\end{definition}
+
+\begin{definition}\label{principalfilter}
+    $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$.
+\end{definition}
+
+%\begin{proposition}\label{principalfilter_domain_inhabited}
+%    Suppose $F$ is a filter on $S$.
+%    Then $S$ is inhabited.
+%\end{proposition}
+
+\begin{proposition}\label{principalfilter_is_filter}
+    Suppose $A\subseteq S$.
+    Suppose $A$ is inhabited.
+    Then $\principalfilter{S}{A}$ is a filter on $S$.
+\end{proposition}
+\begin{proof}
+    $S$ is inhabited. % since $A$ is inhabited and $A\subseteq S$.
+    $\principalfilter{S}{A}$ is a family of subsets of $S$.
+    $S\in \principalfilter{S}{A}$.
+    $\emptyset\notin \principalfilter{S}{A}$.
+    $\principalfilter{S}{A}$ is closed under binary intersections.
+    $\principalfilter{S}{A}$ is upward-closed in $S$.
+    Follows by \cref{filter}.
+\end{proof}
+
+\begin{proposition}\label{principalfilter_elem_generator}
+    Suppose $A\subseteq S$.
+    $A\in\principalfilter{S}{A}$.
+\end{proposition}
+\begin{proof}
+    $A\in\pow{S}$.
+\end{proof}
+
+\begin{proposition}\label{principalfilter_notelem_implies_notsupseteq}
+    Let $X\in\pow{S}$.
+    Suppose $X\notin\principalfilter{S}{A}$.
+    Then $A\not\subseteq X$.
+\end{proposition}
+\begin{proof}
+\end{proof}
+
+\begin{definition}\label{maximalfilter}
+    $F$ is a maximal filter on $S$ iff
+    $F$ is a filter on $S$ and there exists no filter $F'$ on $S$ such that $F\subset F'$.
+\end{definition}
+
+\begin{proposition}\label{principalfilter_singleton_is_filter}
+    Suppose $a\in S$.
+    Then $\principalfilter{S}{\{a\}}$ is a filter on $S$.
+\end{proposition}
+\begin{proof}
+    $\{a\}\subseteq S$.
+    $\{a\}$ is inhabited.
+    Follows by \cref{principalfilter_is_filter}.
+\end{proof}
+
+\begin{proposition}\label{principalfilter_singleton_is_maximal_filter}
+    Suppose $a\in S$.
+    Then $\principalfilter{S}{\{a\}}$ is a maximal filter on $S$.
+\end{proposition}
+\begin{proof}
+    $\{a\}\subseteq S$.
+    $\{a\}$ is inhabited.
+    Thus $\principalfilter{S}{\{a\}}$ is a filter on $S$ by \cref{principalfilter_is_filter}.
+    It suffices to show that there exists no filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$.
+    Suppose not.
+    Take a filter $F'$ on $S$ such that $\principalfilter{S}{\{a\}}\subset F'$.
+    Take $X\in F'$ such that $X\notin \principalfilter{S}{\{a\}}$.
+    $X\in\pow{S}$.
+    Thus $\{a\}\not\subseteq X$ by \cref{principalfilter_notelem_implies_notsupseteq}.
+    Thus $a\notin X$.
+    $\{a\}\in F'$
+        % TODO clean
+        by \cref{principalfilter,elem_subseteq,union_intro_left,subset,union_absorb_subseteq_left,subseteq_refl,powerset_intro}.
+    Thus $\emptyset = X\inter \{a\}$.
+    Hence $\emptyset\in F'$ by \cref{filter}.
+    Follows by \hyperref[filter]{contradiction to the definition of a filter}.
+\end{proof}
diff --git a/library/set/fixpoint.tex b/library/set/fixpoint.tex
new file mode 100644
index 0000000..700295b
--- /dev/null
+++ b/library/set/fixpoint.tex
@@ -0,0 +1,48 @@
+\import{set/powerset.tex}
+\import{function.tex}
+
+\subsection{Fixpoints}
+
+% NOTE: we need to explicitly require that a is an element of the domain,
+% otherwise the emptyset becomes a fixpoint when it's not in the domain.
+\begin{definition}\label{fixpoint}
+    $a$ is a fixpoint of $f$ iff $a\in\dom{f}$ and $f(a) = a$.
+\end{definition}
+
+\begin{definition}\label{subseteqpreserving}
+    $f$ is \subseteq-preserving iff
+    for all $A, B\in\dom{f}$ such that $A\subseteq B$ we have $f(A)\subseteq f(B)$.
+\end{definition}
+
+\begin{theorem}[Knaster--Tarski]\label{knastertarski}
+    Let $f$ be a \subseteq-preserving function from $\pow{A}$ to $\pow{A}$.
+    Then there exists a fixpoint of $f$.
+\end{theorem}
+\begin{proof}
+    $\dom{f} = \pow{A}$.
+    Let $P = \{a\in\pow{A}\mid a\subseteq f(a)\}$.
+    $P\subseteq\pow{A}$.
+    Thus $\unions{P}\in\pow{A}$.
+    Hence $f(\unions{P})\in\pow{A}$ by \cref{funs_type_apply}.
+
+    Show $\unions{P}\subseteq f(\unions{P})$.
+    \begin{subproof}
+        It suffices to show that every element of $\unions{P}$ is an element of $f(\unions{P})$.
+        %
+        Fix $u\in\unions{P}$.
+        %
+        Take $p\in P$ such that $u\in p$.
+        Then $u\in f(p)$.
+        $p\subseteq\unions{P}$.
+        $f(p)\subseteq f(\unions{P})$ by \cref{subseteqpreserving}.
+        Thus $u\in f(\unions{P})$.
+    \end{subproof}
+
+    Now $f(\unions{P})\subseteq f(f(\unions{P}))$ by \cref{subseteqpreserving}.
+    Thus $f(\unions{P})\in P$ by definition.
+
+    Hence $f(\unions{P})\subseteq \unions{P}$.
+
+    Thus $f(\unions{P}) = \unions{P}$ by \cref{subseteq_antisymmetric}.
+    Follows by \cref{fixpoint}.
+\end{proof}
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}
diff --git a/library/set/powerset.tex b/library/set/powerset.tex
new file mode 100644
index 0000000..80da4cb
--- /dev/null
+++ b/library/set/powerset.tex
@@ -0,0 +1,107 @@
+\import{set.tex}
+
+\subsection{Powerset}
+
+\begin{abbreviation}\label{powerset_of}
+    The powerset of $X$ denotes $\pow{X}$.
+\end{abbreviation}
+
+\begin{axiom}%
+\label{pow_iff}
+    $B\in\pow{A}$ iff $B\subseteq A$.
+\end{axiom}
+
+\begin{proposition}\label{powerset_intro}
+    Suppose $A\subseteq B$.
+    Then $A\in\pow{B}$.
+\end{proposition}
+
+\begin{proposition}\label{powerset_elim}
+    Let $A\in\pow{B}$.
+    Then $A\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{powerset_bottom}
+    $\emptyset\in\pow{A}$.
+\end{proposition}
+
+\begin{proposition}\label{powerset_top}
+    $A\in\pow{A}$.
+\end{proposition}
+
+\begin{proposition}\label{unions_subseteq_of_powerset_is_subseteq}
+    Let $A$ be a set.
+    Let $B$ be a subset of $\pow{A}$.
+    Then $\unions{B}\subseteq A$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,powerset_elim,unions_iff}.
+\end{proof}
+
+\begin{corollary}\label{powerset_closed_unions}
+    Let $A$ be a set.
+    Let $B$ be a subset of $\pow{A}$.
+    Then $\unions{B}\in\pow{A}$.
+\end{corollary}
+\begin{proof}
+    Follows by \cref{pow_iff,unions_subseteq_of_powerset_is_subseteq}.
+\end{proof}
+
+\begin{proposition}\label{unions_powerset}
+    $\unions{\pow{A}} = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inters_powerset}
+    $\inters{\pow{A}} = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_powersets_subseteq}
+    $\pow{A}\union\pow{B} \subseteq \pow{A\union B}$.
+\end{proposition}
+\begin{proof}
+    $\pow{A}\subseteq \pow{A}\union\pow{B}$ by \cref{union_upper_left}.
+    $\pow{B}\subseteq \pow{A}\union\pow{B}$ by \cref{union_upper_right}.
+    Follows by \cref{subseteq,pow_iff,powerset_elim,union_iff,subset_transitive}.
+\end{proof}
+
+\begin{proposition}\label{powerset_emptyset}
+    $\pow{\emptyset} = \{\emptyset\}$.
+\end{proposition}
+
+% LATER
+%\begin{proposition}\label{powerset_cons}
+%    Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
+%\end{proposition}
+
+\begin{proposition}\label{powerset_union_subseteq}
+    $\pow{A}\union\pow{B}\subseteq \pow{A\union B}$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_pow_unions}
+    $A\subseteq\pow{\unions{A}}$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{subseteq,pow_iff,unions_intro}.
+\end{proof}
+
+\begin{proposition}\label{unions_pow}
+    $\unions{\pow{A}} = A$.
+\end{proposition}
+
+
+\begin{proposition}\label{unions_elem_pow_iff}
+    $\unions{A}\in\pow{B}$ iff $A\in\pow{\pow{B}}$.
+\end{proposition}
+
+\begin{proposition}\label{pow_inter}
+    $\pow{A\inter B} = \pow{A}\inter\pow{B}$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{setext,inter,pow_iff,subseteq_inter_iff}.
+\end{proof}
diff --git a/library/set/product.tex b/library/set/product.tex
new file mode 100644
index 0000000..bc7d314
--- /dev/null
+++ b/library/set/product.tex
@@ -0,0 +1,118 @@
+\import{set.tex}
+
+\begin{proposition}\label{times_subseteq_left}
+    Suppose $A\subseteq C$. Then $A\times B\subseteq C\times B$.
+\end{proposition}
+\begin{proof}
+    It suffices to show that for all $w\in A\times B$ we have $w\in C\times B$.
+\end{proof}
+
+\begin{proposition}\label{times_subseteq_right}
+    Suppose $B\subseteq D$. Then $A\times B\subseteq A\times D$.
+\end{proposition}
+\begin{proof}
+    It suffices to show that for all $w\in A\times B$ we have $w\in A\times D$.
+\end{proof}
+
+\begin{proposition}\label{inter_times_intro}
+    Suppose $w\in(A\inter B)\times (C\inter D)$.
+    Then $w\in(A\times C)\inter (B\times D)$.
+\end{proposition}
+\begin{proof}
+    Take $a,c$ such that $w = (a, c)$
+        by \cref{times_elem_is_tuple}.
+    Then $a\in A, B$ and $c\in C,D$
+        by \cref{times_tuple_elim,inter}.
+    Thus $w\in (A\times C), (B\times D)$.
+\end{proof}
+
+\begin{proposition}\label{inter_times_elim}
+    Suppose $w\in(A\times C)\inter (B\times D)$.
+    Then $w\in(A\inter B)\times (C\inter D)$.
+\end{proposition}
+\begin{proof}
+    $w\in A\times C$.
+    Take $a, c$ such that $w = (a, c)$.
+    $a\in A, B$ by \cref{inter,times_tuple_elim}.
+    $c\in C, D$ by \cref{inter,times_tuple_elim}.
+    Thus $(a,c) \in (A\inter B)\times (C\inter D)$ by \cref{times,inter_intro}.
+\end{proof}
+
+\begin{proposition}\label{inter_times}
+    $(A\inter B)\times (C\inter D) = (A\times C)\inter (B\times D)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inter_times_right}
+    $(X\inter Y)\times Z = (X\times Z)\inter (Y\times Z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inter_times_left}
+    $X\times (Y\inter Z) = (X\times Y)\inter (X\times Z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_times_intro}
+    Suppose $w\in(A\union B)\times (C\union D)$.
+    Then $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
+\end{proposition}
+\begin{proof}
+    Take $a,c$ such that $w = (a, c)$.
+    $a\in A$ or $a\in B$ by \cref{union_iff,times_tuple_elim}.
+    $c\in C$ or $c\in D$ by \cref{union_iff,times_tuple_elim}.
+    Thus $(a, c)\in (A\times C)$ or $(a, c)\in (B\times D)$ or $(a, c)\in (A\times D)$ or $(a, c)\in (B\times C)$.
+    Thus $(a, c)\in (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
+\end{proof}
+
+\begin{proposition}\label{union_times_elim}
+    Suppose $w\in(A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
+    Then $w\in(A\union B)\times (C\union D)$.
+\end{proposition}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$w\in(A\times C)$.}
+            Take $a, c$ such that $w = (a, c) \land a\in A\land c\in C$ by \cref{times}.
+            Then $a\in A\union B$ and $c\in C\union D$.
+            Follows by \cref{times_tuple_intro}.
+        \caseOf{$w\in(B\times D)$.}
+            Take $b, d$ such that $w = (b, d) \land b\in B\land d\in D$ by \cref{times}.
+            Then $b\in A\union B$ and $d\in C\union D$.
+            Follows by \cref{times_tuple_intro}.
+        \caseOf{$w\in(A\times D)$.}
+            Take $a, d$ such that $w = (a, d) \land a\in A\land d\in D$ by \cref{times}.
+            Then $a\in A\union B$ and $d\in C\union D$.
+            Follows by \cref{times_tuple_intro}.
+        \caseOf{$w\in(B\times C)$.}
+            Take $b, c$ such that $w = (b, c) \land b\in B\land c\in C$ by \cref{times}.
+            Then $b\in A\union B$ and $c\in C\union D$.
+            Follows by \cref{times_tuple_intro}.
+    \end{byCase}
+\end{proof}
+
+\begin{proposition}\label{union_times}
+    $(A\union B)\times (C\union D) = (A\times C)\union (B\times D)\union (A\times D)\union (B\times C)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_times_left}
+    $(X\union Y)\times Z = (X\times Z)\union (Y\times Z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_times_right}
+    $X\times (Y\union Z) = (X\times Y)\union (X\times Z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
diff --git a/library/set/regularity.tex b/library/set/regularity.tex
new file mode 100644
index 0000000..794d34f
--- /dev/null
+++ b/library/set/regularity.tex
@@ -0,0 +1,70 @@
+\import{set.tex}
+
+\section{Regularity}
+
+\begin{abbreviation}\label{elemminimal}
+    $a$ is an \in-minimal element of $A$ iff
+    $a\in A$ and $a\notmeets A$.
+\end{abbreviation}
+
+% We need to first state regularity in this slightly weirder form,
+% so that we can do \in-induction.
+\begin{lemma}%
+\label{regularity_aux}
+    For all $a, A$ such that $a\in A$
+    there exists $b\in A$ such that
+    $b\notmeets A$.
+\end{lemma}
+\begin{proof}[Proof by \in-induction on $a$]
+    \begin{byCase}
+        \caseOf{$a\notmeets b$.}
+            Straightforward.
+        \caseOf{$a\meets b$.}
+            Take $a'$ such that $a'\in a, b$.
+            Straightforward. % we apply the induction hypothesis to a'
+    \end{byCase}
+\end{proof}
+
+\begin{proposition}[Regularity]%
+\label{regularity}
+    Let $A$ be an inhabited set.
+    Then there exists a \in-minimal element of $A$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{regularity_aux,inhabited}.
+\end{proof}
+
+
+% Isabelle/ZF-style foundation for case analysis
+\begin{theorem}[Foundation]\label{foundation}
+    Let $A$ be a set.
+    Then $A = \emptyset$ or there exists $a\in A$
+    such that for all $x\in a$ we have $x\notin A$.
+\end{theorem}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$A = \emptyset$.}
+            Straightforward.
+        \caseOf{$A$ is inhabited.}
+            Take $a$ such that $a$ is a \in-minimal element of $A$.
+            Then for all $x\in a$ we have $x\notin A$.
+    \end{byCase}
+\end{proof}.
+
+\begin{proposition}\label{in_irrefl}
+    For all sets $A$ we have $A\not\in A$.
+\end{proposition}
+\begin{proof}[Proof by \in-induction]
+    Straightforward.
+\end{proof}
+
+\begin{proposition}\label{in_implies_neq}
+    If $a\in A$, then $a\neq A$.
+\end{proposition}
+
+\begin{proposition}\label{in_asymmetric}
+    For all sets $a, b$ such that $a\in b$ we have $b\notin a$.
+\end{proposition}
+\begin{proof}[Proof by \in-induction on $a$]
+    Straightforward.
+\end{proof}
diff --git a/library/set/suc.tex b/library/set/suc.tex
new file mode 100644
index 0000000..3776045
--- /dev/null
+++ b/library/set/suc.tex
@@ -0,0 +1,70 @@
+\import{set/cons.tex}
+\import{set/regularity.tex}
+
+\subsection{Successor}
+
+\begin{definition}\label{suc}
+    $\suc{x} = \cons{x}{x}$.
+\end{definition}
+
+\begin{proposition}\label{suc_intro_self}
+    $x\in\suc{x}$.
+\end{proposition}
+
+\begin{proposition}\label{suc_intro_in}
+    Suppose $x\in y$. Then $x\in\suc{y}$.
+\end{proposition}
+
+\begin{proposition}\label{suc_elim}
+    Suppose $x\in\suc{y}$.
+    Then $x = y$ or $x\in y$.
+\end{proposition}
+
+\begin{proposition}\label{suc_iff}
+    $x\in\suc{y}$ iff $x = y$ or $x\in y$.
+\end{proposition}
+
+\begin{proposition}\label{suc_neq_emptyset}
+    $\suc{x}\neq \emptyset$.
+\end{proposition}
+
+\begin{proposition}\label{suc_subseteq_implies_in}
+    Suppose $\suc{x}\subseteq y$. Then $x\in y$.
+\end{proposition}
+
+\begin{proposition}\label{suc_neq_self}
+    $\suc{x}\neq x$.
+\end{proposition}
+
+\begin{proposition}\label{suc_injective}
+    Suppose $\suc{x} = \suc{y}$. Then $x = y$.
+\end{proposition}
+\begin{proof}
+    Suppose not.
+    $\suc{x}\subseteq \suc{y}$. Hence $x\in\suc{y}$.
+    Then $x\in y$.
+    $\suc{y}\subseteq \suc{x}$. Hence $y\in\suc{x}$.
+    Then $y\in x$.
+    Contradiction.
+\end{proof}
+
+\begin{proposition}\label{subseteq_self_suc_intro}
+    $x\subseteq\suc{x}$.
+\end{proposition}
+
+\begin{proposition}\label{suc_subseteq_intro}
+    Suppose $x\in y$ and $x\subseteq y$.
+    Then $\suc{x}\subseteq y$.
+\end{proposition}
+
+\begin{proposition}\label{suc_subseteq_elim}
+    Suppose $\suc{x}\subseteq y$.
+    Then $x\in y$ and $x\subseteq y$.
+\end{proposition}
+
+\begin{proposition}\label{suc_next_subset}
+    There exists no $z$ such that $x\subset z\subset \suc{x}$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{suc,subset,subseteq,subset_witness,suc_elim}.
+\end{proof}
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}