diff options
Diffstat (limited to 'library/set.tex')
| -rw-r--r-- | library/set.tex | 968 |
1 files changed, 968 insertions, 0 deletions
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} |