From 7559664d56f07bbd1ac5023e6fc1476f62622993 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Thu, 8 Jun 2023 17:57:02 -0600
Subject: [PATCH] Enderton. Ordered pairs.

---
 Bookshelf/Apostol.tex                 |  6 +--
 Bookshelf/Enderton/Set.lean           |  3 +-
 Bookshelf/Enderton/Set.tex            | 61 ++++++++++++++++++++++++++-
 Bookshelf/Enderton/Set/Chapter_3.lean | 12 ++++++
 4 files changed, 76 insertions(+), 6 deletions(-)

diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex
index 95d1847..e04e2cc 100644
--- a/Bookshelf/Apostol.tex
+++ b/Bookshelf/Apostol.tex
@@ -173,10 +173,8 @@ That is to say, for each $k = 1, 2, \ldots, n$, there is a real number $s_k$
   such that $$s(x) = s_k \quad\text{if}\quad x_{k-1} < x < x_k.$$
   Step functions are sometimes called \textbf{piecewise constant functions}.
 
-\vspace{8pt}
-\noindent
-\textit{Note:} At each of the endpoints $x_{k-1}$ and $x_k$ the function must
-  have some well-defined value, but this need not be the same as $s_k$.
+\note{At each of the endpoints $x_{k-1}$ and $x_k$ the function must
+  have some well-defined value, but this need not be the same as $s_k$.}
 
 \begin{definition}
 
diff --git a/Bookshelf/Enderton/Set.lean b/Bookshelf/Enderton/Set.lean
index 52a12d4..231a644 100644
--- a/Bookshelf/Enderton/Set.lean
+++ b/Bookshelf/Enderton/Set.lean
@@ -1,2 +1,3 @@
 import Bookshelf.Enderton.Set.Chapter_1
-import Bookshelf.Enderton.Set.Chapter_2
\ No newline at end of file
+import Bookshelf.Enderton.Set.Chapter_2
+import Bookshelf.Enderton.Set.Chapter_3
\ No newline at end of file
diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index d8875bc..c120ae0 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -2232,7 +2232,7 @@ If not, then under what conditions does equality hold?
 \subsection{\verified{Theorem 3A}}%
 \label{sub:theorem-3a}
 
-\begin{theorem}
+\begin{theorem}[3A]
 
   For any sets $x$, $y$, $u$, and $v$,
     \begin{equation}
@@ -2304,4 +2304,63 @@ If not, then under what conditions does equality hold?
 
 \end{proof}
 
+\subsection{\verified{Lemma 3B}}%
+\label{sub:lemma-3b}
+
+\begin{theorem}[3B]
+
+  If $x \in C$ and $y \in C$, then
+    $\left< x, y \right> \in \powerset{\powerset{C}}$.
+
+\end{theorem}
+
+\begin{proof}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3b}
+
+  Let $C$ be an arbitrary set and $x, y \in C$.
+  Then, by definition of the \nameref{ref:power-set},
+    $\{x\}$ and $\{x, y\}$ are members of $\powerset{C}$.
+  Likewise, $\{\{x\}, \{x, y\}\}$ is a member of $\powerset{\powerset{C}}$.
+  By definition of an \nameref{ref:ordered-pair},
+    $\left< x, y \right> = \{\{x\}, \{x, y\}\}$.
+  This concludes our proof.
+
+\end{proof}
+
+\subsection{\verified{Cartesian Product}}%
+\label{sub:corollary-3c}
+\label{sub:cartesian-product}
+
+\begin{theorem}[3C]
+
+  For any sets $A$ and $B$, there is a set whose members are exactly the
+    pairs $\left< x, y \right>$ with $x \in A$ and $y \in B$.
+
+\end{theorem}
+
+\begin{proof}
+
+  \lean*{Mathlib/SetTheory/ZFC/Basic}{Set.prod}
+
+  \note{The above Lean proof is a definition (i.e. an axiom). It does not prove
+    such a set's existence from first principles.}
+
+  Define $C = A \cup B$.
+  Then for all $x \in A$ and for all $y \in B$, $x$ and $y$ are both in $C$.
+  By \nameref{sub:lemma-3b}, it follows that
+    $\left< x, y \right> \in \powerset{\powerset{C}}$.
+  The \nameref{ref:power-set-axiom} indicates $\powerset{\powerset{C}}$ is
+    indeed a set.
+  Therefore the \nameref{ref:subset-axioms} are applicable.
+  This implies the existence of a set $D$ such that
+    $$\forall z, (z \in D \iff z \in \powerset{\powerset{C}} \land
+      (\exists x, \exists y, x \in A \land y \in B \land
+        z = \left< x, y \right>)).$$
+  By construction $D$ is the set whose members are exactly the pairs
+    $\left< x, y \right>$ with $x \in A$ and $y \in B$.
+
+\end{proof}
+
 \end{document}
diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean
index 1470377..809dfce 100644
--- a/Bookshelf/Enderton/Set/Chapter_3.lean
+++ b/Bookshelf/Enderton/Set/Chapter_3.lean
@@ -1,4 +1,7 @@
 import Mathlib.Data.Set.Basic
+import Mathlib.SetTheory.ZFC.Basic
+
+import Common.Set.OrderedPair
 
 /-! # Enderton.Chapter_3
 
@@ -7,4 +10,13 @@ Relations and Functions
 
 namespace Enderton.Set.Chapter_3
 
+/--
+If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
+-/
+theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
+  : Set.OrderedPair x y ∈ 𝒫 𝒫 C := by
+  have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
+  have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
+  exact Set.mem_mem_imp_pair_subset hxs hxys
+
 end Enderton.Set.Chapter_3
\ No newline at end of file