Enderton. Theorem 3A.

Bookshelf/Enderton/Set.tex

@@ -45,6 +45,18 @@ If two sets have exactly the same members, then they are equal:
 
 \end{axiom}
 
+\section{\defined{Ordered Pair}}%
+\label{ref:ordered-pair}
+
+For any sets $u$ and $v$, the \textbf{ordered pair} $\left< u, v \right>$ is
+  the set $\{\{u\}, \{u, v\}\}$.
+
+\begin{definition}
+
+  \lean*{Common/Set/OrderedPair}{OrderedPair}
+
+\end{definition}
+
 \section{\defined{Pair Set}}%
 \label{ref:pair-set}
 
@@ -2211,4 +2223,85 @@ If not, then under what conditions does equality hold?
 
 \end{proof}
 
+\chapter{Relations and Functions}%
+\label{chap:relations-functions}
+
+\section{Ordered Pairs}%
+\label{sec:ordered-pairs}
+
+\subsection{\verified{Theorem 3A}}%
+\label{sub:theorem-3a}
+
+\begin{theorem}
+
+  For any sets $x$, $y$, $u$, and $v$,
+    \begin{equation}
+      \label{sub:theorem-3a-eq1}
+      \left< u, v \right> = \left< x, y \right> \iff u = x \land v = y.
+    \end{equation}
+
+\end{theorem}
+
+\begin{proof}
+
+  \lean{Common/Set/OrderedPair}{Set.OrderedPair.ext\_iff}
+
+  Let $x$, $y$, $u$, and $v$ be arbitrary sets.
+
+  \paragraph{($\Leftarrow$)}%
+
+    This follows trivially.
+
+  \paragraph{($\Rightarrow$)}%
+
+    Suppose $\left< u, v \right> = \left< x, y \right>$.
+    Then, by definition of an \nameref{ref:ordered-pair},
+      \begin{equation}
+        \label{sub:theorem-3a-eq2}
+        \{\{u\}, \{u, v\}\} = \{\{x\}, \{x, y\}\}.
+      \end{equation}
+    By the \nameref{ref:extensionality-axiom}, it follows
+      $\{u\} \in \{\{x\}, \{x, y\}\}$ and
+      $\{u, v\} \in \{\{x\}, \{x, y\}\}$.
+    That is,
+      $$\{u\} = \{x\} \quad\text{or}\quad \{u\} = \{x, y\}$$
+      and
+      $$\{u, v\} = \{x\} \quad\text{or}\quad \{u, v\} = \{x, y\}.$$
+    There are 4 cases to consider:
+
+    \paragraph{Case 1}%
+
+      Suppose $\{u\} = \{x\}$ and $\{u, v\} = \{x\}$.
+      The former identity implies $u = x$.
+      The latter identity implies $u = v = x$.
+      Then \eqref{sub:theorem-3a-eq2} simplifies to
+        $$\{\{u\}\} = \{\{x\}, \{x, y\}\},$$ meaning $x = y$.
+      Thus $v = y$ as well.
+
+    \paragraph{Case 2}%
+
+      Suppose $\{u\} = \{x\}$ and $\{u, v\} = \{x, y\}$.
+      The former identity implies $u = x$.
+      Substituting into the latter identity yields $\{u, v\} = \{u, y\}$.
+      This holds if and only if $v = y$.
+
+    \paragraph{Case 3}%
+
+      Suppose $\{u\} = \{x, y\}$ and $\{u, v\} = \{x\}$.
+      The former identity implies $x = y = u$.
+      Substituting into the latter yields $\{u, v\} = \{u\}$.
+      Thus $u = v$ which in turn implies $v = y$.
+
+    \paragraph{Case 4}%
+      Suppose $\{u\} = \{x, y\}$ and $\{u, v\} = \{x, y\}$.
+      The former identity implies $x = y = u$.
+      Substituting into the latter yields $\{u, v\} = \{u\}$.
+      This implies $v = u$ which in turn implies $v = y$.
+
+    \paragraph{Conclusion}%
+
+      These cases are exhaustive and each implies that $u = x$ and $v = y$.
+
+\end{proof}
+
 \end{document}

Bookshelf/Enderton/Set/Chapter_2.lean

@@ -1,6 +1,5 @@
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Set.Lattice
-import Mathlib.Tactic.LibrarySearch
 
 import Bookshelf.Enderton.Set.Chapter_1
 import Common.Logic.Basic

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -0,0 +1,10 @@
+import Mathlib.Data.Set.Basic
+
+/-! # Enderton.Chapter_3
+
+Relations and Functions
+-/
+
+namespace Enderton.Set.Chapter_3
+
+end Enderton.Set.Chapter_3

Common/Set.lean

@@ -1,2 +1,4 @@
 import Common.Set.Basic
+import Common.Set.Interval
+import Common.Set.OrderedPair
 import Common.Set.Partition

Common/Set/Basic.lean

@@ -44,6 +44,37 @@ It returns `1` if the specified input belongs to `S` and `0` otherwise.
 def characteristic (S : Set α) (x : α) [Decidable (x ∈ S)] : Nat :=
   if x ∈ S then 1 else 0
 
+/-! ## Equality -/
+
+/--
+If `{x, y} = {x}` then `x = y`.
+-/
+theorem pair_eq_singleton_mem_imp_eq_self {x y : α}
+  (h : {x, y} = ({x} : Set α)) : y = x := by
+  rw [Set.ext_iff] at h
+  have := h y
+  simp at this
+  exact this
+
+/--
+If `{x, y} = {z}` then `x = y = z`.
+-/
+theorem pair_eq_singleton_mem_imp_eq_all {x y z : α}
+  (h : {x, y} = ({z} : Set α)) : x = z ∧ y = z := by
+  have h' := h
+  rw [Set.ext_iff] at h'
+  have hz := h' z
+  simp at hz
+  apply Or.elim hz
+  · intro hzx
+    rw [← hzx] at h
+    have := pair_eq_singleton_mem_imp_eq_self h
+    exact ⟨hzx.symm, this⟩
+  · intro hzy
+    rw [← hzy, Set.pair_comm] at h
+    have := pair_eq_singleton_mem_imp_eq_self h
+    exact ⟨this, hzy.symm⟩
+
 /-! ## Subsets -/
 
 /--

Common/Set/OrderedPair.lean

@@ -0,0 +1,93 @@
+import Mathlib.Data.Set.Basic
+
+import Common.Logic.Basic
+import Common.Set.Basic
+
+namespace Set
+
+/--
+Kazimierz Kuratowski's definition of an ordered pair.
+-/
+def OrderedPair (x y : α) : Set (Set α) := {{x}, {x, y}}
+
+namespace OrderedPair
+
+theorem ext_iff {x y u v : α}
+  : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by
+  unfold OrderedPair
+  apply Iff.intro
+  · intro h
+    have h' := h
+    rw [Set.ext_iff] at h'
+    have hu := h' {u}
+    have huv := h' {u, v}
+    simp only [mem_singleton_iff, mem_insert_iff, true_or, iff_true] at hu
+    simp only [mem_singleton_iff, mem_insert_iff, or_true, iff_true] at huv
+    apply Or.elim hu
+    · apply Or.elim huv
+      · -- #### Case 1
+        -- `{u} = {x}` and `{u, v} = {x}`.
+        intro huv_x hu_x
+        rw [singleton_eq_singleton_iff] at hu_x
+        rw [hu_x] at huv_x
+        have hx_v := pair_eq_singleton_mem_imp_eq_self huv_x
+        rw [hu_x, hx_v] at h
+        simp only [mem_singleton_iff, insert_eq_of_mem] at h
+        have := pair_eq_singleton_mem_imp_eq_self $
+          pair_eq_singleton_mem_imp_eq_self h
+        rw [← hx_v] at this
+        exact ⟨hu_x.symm, this⟩
+      · -- #### Case 2
+        -- `{u} = {x}` and `{u, v} = {x, y}`.
+        intro huv_xy hu_x
+        rw [singleton_eq_singleton_iff] at hu_x
+        rw [hu_x] at huv_xy
+        by_cases hx_v : x = v
+        · rw [hx_v] at huv_xy
+          simp at huv_xy
+          have := pair_eq_singleton_mem_imp_eq_self huv_xy.symm
+          exact ⟨hu_x.symm, this⟩
+        · rw [Set.ext_iff] at huv_xy
+          have := huv_xy v
+          simp at this
+          apply Or.elim this
+          · intro hv_x
+            rw [hu_x, ← hv_x] at h
+            simp at h
+            have := pair_eq_singleton_mem_imp_eq_self $
+              pair_eq_singleton_mem_imp_eq_self h
+            exact ⟨hu_x.symm, this⟩
+          · intro hv_y
+            exact ⟨hu_x.symm, hv_y.symm⟩
+    · apply Or.elim huv
+      · -- #### Case 3
+        -- `{u} = {x, y}` and `{u, v} = {x}`.
+        intro huv_x hu_xy
+        rw [Set.ext_iff] at huv_x
+        have hu_x := huv_x u
+        have hv_x := huv_x v
+        simp only [mem_singleton_iff, mem_insert_iff, true_or, true_iff] at hu_x
+        simp only [mem_singleton_iff, mem_insert_iff, or_true, true_iff] at hv_x
+        rw [← hu_x] at hu_xy
+        have := pair_eq_singleton_mem_imp_eq_self hu_xy.symm
+        rw [hu_x, ← hv_x] at this
+        exact ⟨hu_x.symm, this⟩
+      · -- #### Case 4
+        -- `{u} = {x, y}` and `{u, v} = {x, y}`.
+        intro huv_xy hu_xy
+        rw [Set.ext_iff] at hu_xy
+        have hx_u := hu_xy x
+        have hy_u := hu_xy y
+        simp only [mem_singleton_iff, mem_insert_iff, true_or, iff_true] at hx_u
+        simp only [mem_singleton_iff, mem_insert_iff, or_true, iff_true] at hy_u
+        rw [hx_u, hy_u] at huv_xy
+        simp only [mem_singleton_iff, insert_eq_of_mem] at huv_xy
+        have := pair_eq_singleton_mem_imp_eq_self huv_xy
+        rw [← this] at hy_u
+        exact ⟨hx_u, hy_u⟩
+  · intro h
+    rw [h.left, h.right]
+
+end OrderedPair
+
+end Set