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.tex | 968 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 968 insertions(+)
 create mode 100644 library/set.tex

(limited to 'library/set.tex')

diff --git a/library/set.tex b/library/set.tex
new file mode 100644
index 0000000..33e5af4
--- /dev/null
+++ b/library/set.tex
@@ -0,0 +1,968 @@
+\section{Sets}
+
+\begin{abbreviation}\label{ni}
+    $A\ni a$ iff $a\in A$.
+\end{abbreviation}
+
+\subsection{Extensionality}
+
+The axiom of set extensionality says that sets are determined by their \textit{extension},
+that is, two sets are equal iff they have the same elements.
+%
+\begin{axiom}[Set extensionality]\label{setext}
+    Suppose for all $a$ we have $a\in A$ iff $a\in B$.
+    Then $A = B$.
+\end{axiom}
+
+This axiom is also available as the justification “{\ldots\ by set extensionality}”,
+which applies it to goals of the form “$A = B$” and  “$A \neq B$”.
+
+\begin{proposition}[Witness for disequality]%
+\label{neq_witness}
+    Suppose $A\neq B$.
+    Then there exists $c$ such that
+    either $c\in A$ and $c\not\in B$
+    or $c\not\in A$ and $c\in B$.
+\end{proposition}
+\begin{proof}
+    Suppose not. Then $A = B$ by set extensionality. Contradiction.
+\end{proof}
+
+
+
+\subsection{Subsets}
+
+\begin{definition}\label{subseteq}
+    $A\subseteq B$ iff
+    for all $a\in A$ we have $a\in B$.
+\end{definition}
+
+\begin{abbreviation}\label{is_subset}
+    $A$ is a subset of $B$ iff $A\subseteq B$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{supseteq}
+    $B\supseteq A$ iff $A\subseteq B$.
+\end{abbreviation}
+
+\begin{proposition}%
+\label{subseteq_refl}
+    $A\subseteq A$.
+\end{proposition}
+
+\begin{proposition}%
+\label{subseteq_antisymmetric}
+    Suppose $A\subseteq B\subseteq A$.
+    Then $A = B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{elem_subseteq}
+    Suppose $a\in A\subseteq B$.
+    Then $a\in B$.
+\end{proposition}
+
+\begin{proposition}%
+\label{not_in_subseteq}
+    Suppose $A\subseteq B$ and $c\notin B$.
+    Then $c\notin A$.
+\end{proposition}
+
+\begin{proposition}%
+\label{subseteq_transitive}
+    Suppose $A\subseteq B\subseteq C$.
+    Then $A\subseteq C$.
+\end{proposition}
+
+\begin{definition}\label{subset}
+    $A\subset B$ iff
+    $A\subseteq B$ and $A\neq B$.
+\end{definition}
+
+\begin{proposition}\label{subset_irrefl}
+    $A\not\subset A$.
+\end{proposition}
+
+\begin{proposition}\label{subset_transitive}
+    Suppose $A\subseteq B\subseteq C$.
+    Then $A\subseteq C$.
+\end{proposition}
+
+\begin{proposition}\label{subset_witness}
+    Suppose $A\subset B$.
+    Then there exists $b\in B$ such that $b\notin A$.
+\end{proposition}
+\begin{proof}
+    $A\subseteq B$ and $A\neq B$.
+\end{proof}
+
+\begin{abbreviation}\label{family_of_subsets}
+    $F$ is a family of subsets of $X$ iff
+    for all $A\in F$ we have $A\subseteq X$.
+\end{abbreviation}
+
+
+\subsection{The empty set}
+
+\begin{axiom}%
+\label{notin_emptyset}
+    For all $a$ we have $a\notin\emptyset$.
+\end{axiom}
+
+\begin{definition}\label{inhabited}
+    $A$ is inhabited iff
+    there exists $a$ such that $a\in A$.
+\end{definition}
+
+\begin{abbreviation}\label{empty}
+    $A$ is empty iff $A$ is not inhabited.
+\end{abbreviation}
+
+%\begin{proposition}%
+%\label{inhabited_iff_nonempty}
+%    $A$ is inhabited iff $A$ is not empty.
+%\end{proposition}
+
+\begin{proposition}%
+\label{empty_eq}
+    If $x$ and $y$ are empty, then $x = y$.
+\end{proposition}
+
+\begin{proposition}%
+\label{emptyset_subseteq}
+    For all $a$ we have $\emptyset \subseteq a$.
+    % LATER $\emptyset$ is a subset of every set.
+\end{proposition}
+
+\begin{proposition}%
+\label{subseteq_emptyset_iff}
+    $A\subseteq \emptyset$ iff $A = \emptyset$.
+\end{proposition}
+
+
+\subsection{Disjointness of sets}
+
+\begin{definition}\label{disjoint}
+    $A$ is disjoint from $B$ iff there exists no $a$ such that $a\in A, B$.
+\end{definition}
+
+\begin{abbreviation}\label{notmeets}
+    $A\notmeets B$ iff $A$ is disjoint from $B$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{meets}
+    $A\meets B$ iff $A$ is not disjoint from $B$.
+\end{abbreviation}
+
+\begin{proposition}%
+\label{disjoint_symmetric}
+    If $A$ is disjoint from $B$, then $B$ is disjoint from $A$.
+\end{proposition}
+
+
+
+
+
+\subsection{Unordered pairing and set adjunction}
+
+Finite set expressions are desugared to
+iterated application of $\operatorname{\textsf{cons}}$ to $\emptyset$.
+Thus $\{x,y,z\}$ is an abbreviaton of
+$\cons{x}{\cons{y}{\cons{z}{\emptyset}}}$.
+The $\operatorname{\textsf{cons}}$ operation is determined by the following axiom:
+%
+\begin{axiom}\label{cons_iff}
+    $x\in \cons{y}{X}$ iff $x = y$ or $x\in X$.
+\end{axiom}
+
+\begin{proposition}\label{cons_left}
+    $x\in \cons{x}{X}$.
+\end{proposition}
+
+\begin{proposition}\label{cons_right}
+    If $y\in X$, then $y\in \cons{x}{X}$.
+\end{proposition}
+
+
+% Unordered pairs:
+
+\begin{proposition}\label{upair_intro_left}
+    $a\in\{a,b\}$.
+\end{proposition}
+
+\begin{proposition}\label{upair_intro_right}
+    $b\in\{a,b\}$.
+\end{proposition}
+
+\begin{proposition}\label{upair_elim}
+    Suppose $c\in\{a,b\}$. Then $a = c$ or $b = c$.
+\end{proposition}
+
+\begin{proposition}\label{upair_iff}
+    $c\in\{a,b\}$ iff $a = c$ or $b = c$.
+\end{proposition}
+
+
+% Singletons:
+
+\begin{proposition}\label{singleton_intro}
+    $a\in\{a\}$.
+\end{proposition}
+
+\begin{proposition}\label{singleton_elim}
+    If $a\in\{b\}$, then $a = b$.
+\end{proposition}
+
+\begin{proposition}\label{singleton_iff}
+    $a\in\{b\}$ iff $a = b$.
+\end{proposition}
+
+\begin{abbreviation}\label{subsingleton}
+    $A$ is a subsingleton iff for all $a, b\in A$ we have $a = b$.
+\end{abbreviation}
+
+\begin{proposition}\label{singleton_inhabited}
+    $\{a\}$ is inhabited.
+\end{proposition}
+
+\begin{proposition}\label{singleton_iff_inhabited_subsingleton}
+    Let $A$ be a subsingleton.
+    Let $a\in A$.
+    Then $A = \{a\}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{singleton_subset_intro}
+    Suppose $a\in C$.
+    Then $\{a\}\subseteq C$.
+\end{proposition}
+
+\begin{proposition}\label{singleton_subset_elim}
+    Suppose $\{a\}\subseteq C$.
+    Then $a\in C$.
+\end{proposition}
+
+
+\subsection{Union and intersection}
+
+\subsubsection{Union of a set}
+
+\begin{axiom}\label{unions_iff}
+    $z\in\unions{X}$ iff there exists $Y\in X$ such that $z\in Y$.
+\end{axiom}
+
+
+\begin{proposition}%
+\label{unions_intro}
+    Suppose $A\in B\in C$.
+    Then $A\in\unions{C}$.
+\end{proposition}
+\begin{proof}
+    There exists $B\in C$ such that $A\in B$.
+\end{proof}
+
+\begin{proposition}%
+\label{unions_emptyset}
+    $\unions{\emptyset} = \emptyset$.
+\end{proposition}
+
+\begin{proposition}\label{unions_family}
+    Let $F$ be a family of subsets of $X$.
+    Then $\unions{F}\subseteq X$.
+\end{proposition}
+
+\begin{abbreviation}\label{closedunderunions}
+    $T$ is closed under arbitrary unions
+    iff for every subset $M$ of $T$ we have $\unions{M}\in T$.
+\end{abbreviation}
+
+\subsubsection{Intersection of a set}
+
+\begin{definition}\label{inters}
+    $\inters{A} = \{ x\in\unions{A}\mid \text{for all $a\in A$ we have $x\in a$} \}$.
+\end{definition}
+
+\begin{proposition}\label{inters_iff_forall}
+    $z\in\inters{X}$ iff $X$ is inhabited and for all $Y\in X$ we have $z\in Y$.
+\end{proposition}
+
+\begin{proposition}%
+\label{inters_intro}
+    Suppose $C$ is inhabited.
+    Suppose for all $B\in C$ we have $A\in B$.
+    Then $A\in\inters{C}$.
+\end{proposition}
+
+\begin{proposition}\label{inters_destr}
+    Suppose $A\in\inters{C}$.
+    Suppose $B\in C$.
+    Then $A\in B$.
+\end{proposition}
+
+\begin{proposition}\label{inters_greatest}
+    Suppose $A$ is inhabited.
+    Suppose for all $a\in A$ we have $C\subseteq a$.
+    Then $C\subseteq\inters{A}$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_inters_iff}
+    Suppose $A$ is inhabited.
+    Then $C\subseteq\inters{A}$ iff for all $a\in A$ we have $C\subseteq a$.
+\end{proposition}
+
+\begin{proposition}\label{inters_subseteq_elem}
+    Let $B\in A$.
+    Then $\inters{A}\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{inters_singleton}
+    $\inters{\{a\}} = a$.
+\end{proposition}
+\begin{proof}
+    Every element of $a$ is an element of $\inters{\{a\}}$
+        by \cref{inters_iff_forall,singleton_iff,singleton_inhabited}.
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inters_emptyset}
+    $\inters{\{\emptyset\}} = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\subsubsection{Binary union}
+
+\begin{axiom}\label{union_iff}
+    Let $A, B$ be sets.
+    $a\in A\union B$ iff $a\in A$ or $a\in B$.
+\end{axiom}
+
+\begin{proposition}\label{union_intro_left}
+    If $c\in A$, then $c\in A\union B$.
+\end{proposition}
+
+\begin{proposition}\label{union_intro_right}
+    If $c\in B$, then $c\in A\union B$.
+\end{proposition}
+
+\begin{proposition}\label{union_as_unions}
+    $\unions{\{x,y\}} = x\union y$.
+\end{proposition}
+\begin{proof}
+    %For all z we have
+    %\begin{align*}
+    %    z\in \unions{\{x,y\}}
+    %    &\iff \exists Z\in\{x,y\}. z\in Z
+    %\end{align*}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}[Commutativity of union]%
+\label{union_comm}
+    $A\union B = B\union A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}[Associativity of union]%
+\label{union_assoc}
+    $(A\union B)\union C = A\union (B\union C)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}[Idempotence of union]%
+\label{union_idempotent}
+    $A\union A = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{subseteq_union_iff}
+    $A\union B\subseteq C$ iff $A\subseteq C$ and $B\subseteq C$.
+\end{proposition}
+
+\begin{proposition}\label{union_upper_left}
+    $A\subseteq A\union B$.
+\end{proposition}
+
+\begin{proposition}\label{union_upper_right}
+    $B\subseteq A\union B$.
+\end{proposition}
+
+\begin{proposition}\label{union_subseteq_union}
+    Suppose $A\subseteq C$ and $B\subseteq D$.
+    Then $A\union B\subseteq C\union D$.
+\end{proposition}
+
+\begin{proposition}%
+\label{union_emptyset}
+    $A\union\emptyset = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+
+\begin{proposition}%
+\label{union_emptyset_intro}
+    Suppose $A = \emptyset$ and $B = \emptyset$. Then $A\union B = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{union_emptyset_elim_left}
+    Suppose $A\union B = \emptyset$. Then $A = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{union_emptyset_elim_right}
+    Suppose $A\union B = \emptyset$. Then $B = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{union_absorb_subseteq_left}
+    Suppose $A\subseteq B$. Then $A\union B = B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{union_absorb_subseteq_right}
+    Suppose $A\subseteq B$. Then $B\union A = B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{union_eq_self_implies_subseteq}
+    If $A\union B = B$, then $A\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{unions_cons}
+    $\unions{\cons{b}{A}} = b\union\unions{A}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_cons}
+    $\cons{b}{A} \union C = \cons{b}{A\union C}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_absorb_left}
+    $A\union (A\union B) = A\union B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_absorb_right}
+    $(A\union B)\union B = A\union B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{union_comm_left}
+    $A\union (B\union C) = B\union (A\union C)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{abbreviation}\label{closedunderunion}
+    $T$ is closed under binary unions
+    iff for every $U,V\in T$ we have $U\union V\in T$.
+\end{abbreviation}
+
+
+\subsubsection{Binary intersection}
+
+\begin{definition}\label{inter}
+    $A\inter B = \{ a \in A \mid a\in B\}$.
+\end{definition}
+
+\begin{proposition}\label{inter_intro}
+    If $c\in A, B$, then $c\in A\inter B$.
+\end{proposition}
+
+\begin{proposition}\label{inter_elim_left}
+    If $c\in A\inter B$, then $c\in A$.
+\end{proposition}
+
+\begin{proposition}\label{inter_elim_right}
+    If $c\in A\inter B$, then $c\in B$.
+\end{proposition}
+
+\begin{proposition}\label{inter_as_inters}
+    $\inters{\{A,B\}} = A\inter B$.
+\end{proposition}
+\begin{proof}
+    $\{A,B\}$ is inhabited.
+    Thus for all $c$ we have $c\in\inters{\{A,B\}}$ iff $c\in A\inter B$
+        by \cref{inters_iff_forall,inter,upair_iff}.
+    %Thus $\inters{\{A,B\}} = A\inter B$ by \hyperref[setext]{extensionality}.
+    Follows by \hyperref[setext]{extensionality}.
+\end{proof}
+
+
+\begin{proposition}[Commutativity of intersection]%
+\label{inter_comm}
+    $A\inter B = B\inter A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}[Associativity of intersection]%
+\label{inter_assoc}
+    $(A\inter B)\inter C = A\inter (B\inter C)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}[Idempotence of intersection]%
+\label{inter_idempotent}
+    $A\inter A = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{inter_subseteq}
+    $A\inter B\subseteq A$.
+\end{proposition}
+
+\begin{proposition}%
+\label{inter_emptyset}
+    $A\inter\emptyset = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{inter_absorb_supseteq_right}
+    Suppose $A\subseteq B$. Then $A\inter B = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{inter_absorb_supseteq_left}
+    Suppose $A\subseteq B$. Then $B\inter A = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{inter_eq_left_implies_subseteq}
+    Suppose $A\inter B = A$. Then $A\subseteq B$.
+\end{proposition}
+
+\begin{proposition}%
+\label{subseteq_inter_iff}
+    $C\subseteq A\inter B$ iff $C\subseteq A$ and $C\subseteq B$.
+\end{proposition}
+
+\begin{proposition}%
+\label{inter_lower_left}
+    $A\inter B \subseteq A$.
+\end{proposition}
+
+\begin{proposition}%
+\label{inter_lower_right}
+    $A\inter B \subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{inter_absorb_left}
+    $A\inter (A\inter B) = A\inter B$.
+\end{proposition}
+\begin{proof} Follows by set extensionality. \end{proof}
+
+\begin{proposition}%
+\label{inter_absorb_right}
+    $(A\inter B) \inter B = A\inter B$.
+\end{proposition}
+\begin{proof} Follows by set extensionality. \end{proof}
+
+\begin{proposition}\label{inter_comm_left}
+    $A\inter (B\inter C) = B\inter (A\inter C)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{abbreviation}\label{closedunderinter}
+    $T$ is closed under binary intersections
+    iff for every $U,V\in T$ we have $U\inter V\in T$.
+\end{abbreviation}
+
+\subsubsection{Interaction of union and intersection}
+
+\begin{proposition}[Binary intersection over binary union]%
+\label{inter_distrib_union}
+    $x\inter (y\union z) = (x\inter y)\union (x\inter z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}[Binary union over binary intersection]%
+\label{union_distrib_inter}
+    $x\union (y\inter z) = (x\union y)\inter (x\union z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+% Halmos, Naive Set Theory, page 16
+\begin{proposition}\label{union_inter_assoc_intro}
+    Suppose $C\subseteq A$.
+    Then $(A\inter B)\union C = A\inter (B\union C)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+% Halmos, Naive Set Theory, page 16
+\begin{proposition}\label{union_inter_assoc_elim}
+    Suppose $(A\inter B)\union C = A\inter (B\union C)$.
+    Then $C\subseteq A$.
+\end{proposition}
+
+% From Isabelle/ZF equalities theory
+\begin{proposition}\label{union_inter_crazy}
+    $(A\inter B)\union (B\inter C)\union (C\inter A)
+    =
+    (A\union B)\inter (B\union C)\inter (C\union A)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+
+\begin{proposition}[Intersection over binary union]\label{inters_distrib_union}
+    Suppose $A$ and $B$ are inhabited.
+    Then $\inters{A\union B} = (\inters{A})\inter\inters{B}$.
+\end{proposition}
+\begin{proof}
+    $A\union B$ is inhabited.
+    Thus for all $c$ we have $c\in\inters{A\union B}$ iff $c\in(\inters{A})\inter\inters{B}$
+        by \cref{inter,union_iff,inters_iff_forall}.
+    Follows by \hyperref[setext]{set extensionality}. % We only need the actual setext axiom here, not the tactic.
+\end{proof}
+
+\subsection{Set difference}
+
+\begin{definition}\label{setminus}
+    $A\setminus B = \{ a \in A \mid a\not\in B\}$.
+\end{definition}
+
+\begin{proposition}\label{setminus_intro}
+    If $a\in A$ and $a\notin B$, then $a\in A\setminus B$.
+\end{proposition}
+
+\begin{proposition}\label{setminus_elim_left}
+    If $a\in A\setminus B$, then $a\in A$.
+\end{proposition}
+
+\begin{proposition}\label{setminus_elim_right}
+    If $a\in A\setminus B$, then $a\notin B$.
+\end{proposition}
+
+\begin{proposition}\label{setminus_emptyset}
+    $x\setminus \emptyset = x$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{emptyset_setminus}
+    $\emptyset\setminus x = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{setminus_self}
+    $x\setminus x = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+% NOTE: This theorem tends to show up spuriously in ATP proofs!
+% Getting rid of it via explicit \cref{..} can save time.
+\begin{proposition}\label{setminus_setminus}
+    $x\setminus (x\setminus y) = x\inter y$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{double_relative_complement}
+    Suppose $y\subseteq x$.
+    $x\setminus (x\setminus y) = y$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{setminus_setminus,inter_absorb_supseteq_left}.
+\end{proof}
+
+\begin{proposition}\label{setminus_inter}
+    $x\setminus (y\inter z) = (x\setminus y)\union (x\setminus z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{setminus_union}
+    $x\setminus (y\union z) = (x\setminus y)\inter (x\setminus z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{inter_setminus}
+    $x\inter (y\setminus z) = (x\inter y)\setminus (x\inter z)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}%
+\label{difference_with_proper_subset_is_inhabited}
+    Let $A, B$ be sets.
+    Suppose $A\subset B$.
+    Then $B\setminus A$ is inhabited.
+\end{proposition}
+\begin{proof}
+    Take $b$ such that $b\in B$ and $b\notin A$.
+    Then $b\in B\setminus A$.
+\end{proof}
+
+\begin{proposition}\label{setminus_subseteq}
+    $B\setminus A\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_setminus}
+    Suppose $C\subseteq A$.
+    Suppose $C\inter B = \emptyset$.
+    Then $C\subseteq A\setminus B$.
+\end{proposition}
+
+
+\begin{proposition}\label{subseteq_implies_setminus_supseteq}
+    Suppose $A\subseteq B$.
+    Then $C\setminus A\supseteq C\setminus B$.
+\end{proposition}
+
+\begin{proposition}\label{setminus_absorb_right}
+    Suppose $A\inter B = \emptyset$.
+    Then $A\setminus B = A$.
+\end{proposition}
+
+\begin{proposition}\label{setminus_eq_emptyset_iff_subseteq}
+    $A\setminus B = \emptyset$ iff $A\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_setminus_cons_intro}
+    Suppose $B\subseteq A\setminus C$ and $c\notin B$. Then $B\subseteq A\setminus\cons{c}{C}$.
+\end{proposition}
+
+\begin{proposition}\label{subseteq_setminus_cons_elim}
+    Suppose $B\subseteq A\setminus\cons{c}{C}$. Then $B\subseteq A\setminus C$ and $c\notin B$.
+\end{proposition}
+
+\begin{proposition}\label{setminus_cons}
+    $A\setminus \cons{a}{B} = (A\setminus \{a\})\setminus B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+\begin{proposition}\label{setminus_cons_flip}
+    $A\setminus \cons{a}{B} = (A\setminus B)\setminus \{a\}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{setminus_disjoint}
+    $A\inter (B\setminus A) = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{setminus_partition}
+    Suppose $A\subseteq B$.
+    $A\union (B\setminus A) = B$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{subseteq_union_setminus}
+    $A\subseteq B\union (A\setminus B)$.
+\end{proposition}
+
+\begin{proposition}\label{double_complement}
+    Suppose $A\subseteq B\subseteq C$.
+    Then $B\setminus (C\setminus A) = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{double_complement_union}
+    Then $(A\union B)\setminus (B\setminus A) = A$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{setminus_eq_inter_complement}
+    Suppose $A, B\subseteq C$.
+    Then $A\setminus B = A\inter (C\setminus B)$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\subsection{Tuples}
+
+As with unordered pairs,
+orderd pairs are a primitive construct and
+$n$-tuples desugar to iterated applications of the
+primitive operator $({-},{-})$.
+For example $(a, b, c, d)$ equals $(a, (b, (c, d)))$ by definition.
+While ordered pairs could be encoded set-theoretically, %(choosing Kuratowski's, Hausdorff's, or Wiener's encoding),
+we simply postulate the defining property to prevent misguiding
+proof automation.
+
+\begin{axiom}\label{pair_eq_iff}
+    $(a, b) = (a', b')$ iff $a = a'\land b = b'$.
+\end{axiom}
+
+\begin{axiom}\label{pair_neq_emptyset}
+    $(a, b) \neq \emptyset$.
+\end{axiom}
+
+\begin{axiom}\label{pair_neq_fst}
+    $(a, b) \neq a$.
+\end{axiom}
+
+\begin{axiom}\label{pair_neq_snd}
+    $(a, b) \neq b$.
+\end{axiom}
+
+Repeated application of the defining property of pairs yields the defining property of
+all tuples.
+
+\begin{proposition}\label{triple_eq_iff}
+    $(a, b, c) = (a', b', c')$ iff $a = a' \land b = b'\land c = c'$.
+\end{proposition}
+
+There are primitive projections $\fst{}$ and $\snd{}$ that satisfy the following axioms.
+
+\begin{axiom}\label{fst_eq}
+    $\fst{(a, b)} = a$.
+\end{axiom}
+
+\begin{axiom}\label{snd_eq}
+    $\snd{(a, b)} = b$.
+\end{axiom}
+
+\begin{proposition}\label{pair_eq_pair_of_proj}
+    $(a, b) = (\fst{(a,b)},\snd{(a,b)})$.
+\end{proposition}
+
+
+\begin{definition}\label{times}
+    $A\times B = \{ (a,b) \mid a\in A, b\in B \}$.
+\end{definition}
+
+\begin{proposition}\label{times_tuple_elim}
+    Suppose $(x, y)\in X\times Y$. Then $x\in X$ and $y\in Y$.
+\end{proposition}
+\begin{proof}
+    Take $x', y'$ such that $x'\in X\land y'\in Y \land (x, y) = (x', y')$
+        by \cref{times}.
+    Then $x = x'$ and $y = y'$ by \cref{pair_eq_iff}.
+\end{proof}
+
+\begin{proposition}\label{times_tuple_intro}
+    Suppose $x\in X$ and $y\in Y$. Then $(x, y)\in X\times Y$.
+\end{proposition}
+
+\begin{proposition}\label{times_empty_left}
+    $\emptyset\times Y = \emptyset$.
+\end{proposition}
+
+\begin{proposition}\label{times_empty_right}
+    $X\times \emptyset = \emptyset$.
+\end{proposition}
+
+\begin{proposition}\label{times_empty_iff}
+    $X\times Y$ is empty iff $X$ is empty or $Y$ is empty.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{inhabited,times}.
+\end{proof}
+
+\begin{proposition}\label{fst_type}
+    Suppose $c\in A\times B$. Then $\fst{c}\in A$.
+\end{proposition}
+\begin{proof}
+    Take $a, b$ such that $c = (a, b)$ and $a\in A$
+        by \cref{times}.
+    $a = \fst{c}$
+        by \cref{fst_eq}.
+\end{proof}
+
+\begin{proposition}\label{snd_type}
+    Suppose $c\in A\times B$. Then $\snd{c}\in B$.
+\end{proposition}
+\begin{proof}
+    Take $a, b$ such that $c = (a, b)$ and $b\in B$
+        by \cref{times}.
+    $b = \snd{c}$
+        by \cref{snd_eq}.
+\end{proof}
+
+\begin{proposition}\label{times_elem_is_tuple}
+    Suppose $p\in X\times Y$. Then there exist $x, y$
+    such that $x\in X$ and $y\in Y$ and $p = (x, y)$.
+\end{proposition}
+
+
+\begin{proposition}\label{times_proj_elim}
+    Suppose $p\in X\times Y$. Then $\fst{p}\in X$ and $\snd{p}\in Y$.
+\end{proposition}
-- 
cgit v1.2.3