Enderton. Move Kuratowski's definition of an ordered pair into chapter; not

likely to be used outside this book.

Bookshelf/Enderton/Set.tex

@@ -2244,7 +2244,8 @@ If not, then under what conditions does equality hold?
 
 \begin{proof}
 
-  \lean{Common/Set/OrderedPair}{Set.OrderedPair.ext\_iff}
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.OrderedPair.ext\_iff}
 
   Let $x$, $y$, $u$, and $v$ be arbitrary sets.
 
@@ -2518,7 +2519,7 @@ Show that there is no set to which every ordered pair belongs.
 
 \end{proof}
 
-\subsection{\partial{Exercise 5.5a}}%
+\subsection{\unverified{Exercise 5.5a}}%
 \label{sub:exercise-5.5a}
 
 Assume that $A$ and $B$ are given sets, and show that there exists a set $C$
@@ -2581,32 +2582,54 @@ In other words, show that $\{\{x\} \times B \mid x \in A\}$ is a set.
 
 \end{proof}
 
-\subsection{\partial{Exercise 5.5b}}%
+\subsection{\verified{Exercise 5.5b}}%
 \label{sub:exercise-5.5b}
 
 With $A$, $B$, and $C$ as above, show that $A \times B = \bigcup C$.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_5\_5b}
+
   Let $A$ and $B$ be arbitrary sets.
   We want to show that
     \begin{equation}
       \label{sub:exercise-5.5b-eq1}
       A \times B = \bigcup\; \{\{x\} \times B \mid x \in A\}.
     \end{equation}
-  Note that \nameref{sub:cartesian-product} and \nameref{sub:exercise-5.5a}
+  The left-hand side of \eqref{sub:exercise-5.5b-eq1} is a set by virtue of
-    prove the left- and right-hand sides of \eqref{sub:exercise-5.5b-eq1} are
+    \nameref{sub:cartesian-product}.
-    sets respectively.
+  The right-hand side of \eqref{sub:exercise-5.5b-eq1} is a set by virtue of
-  Then
+    \nameref{sub:exercise-5.5a}.
-    \begin{align*}
+  We prove the set on each side is a subset of the other.
-      A \times B
+
-        & = \{ y \mid \exists x \in A, \exists b \in B, y = \left< x, b \right> \} \\
+  \paragraph{($\subseteq$)}%
-        & = \{ y \mid \exists b \in B, \exists x \in A, y = \left< x, b \right> \} \\
+
-        & = \{ y \mid \exists b \in B, y \in \{ \left< x, b \right> \mid x \in A \} \} \\
+    Let $c \in A \times B$.
-        & = \{ y \mid y \in \{ \left< x, b \right> \mid x \in A \land b \in B \} \} \\
+    Then there exists some $a \in A$ and $b \in B$ such that
-        & = \{ y \mid \exists z \in \{\{x\} \times B \mid x \in A \}, y \in z \} \\
+      $c = \left< a, b \right>$.
-        & = \bigcup \{\{x\} \times B \mid x \in A \}.
+    Thus $c \in \{a\} \times B$.
-    \end{align*}
+    We also note $\{a\} \times B \in \{\{x\} \times B \mid x \in A\}$,
+      specifically when $x = a$.
+    Therefore, by the \nameref{ref:union-axiom},
+      $c \in \bigcup\;\{\{x\} \times B \mid x \in A\}$.
+
+  \paragraph{($\supseteq$)}%
+
+    Let $c \in \bigcup\; \{\{x\} \times B \mid x \in A\}$.
+    By the \nameref{ref:union-axiom}, there exists some
+      $b \in \{\{x\} \times B \mid x \in A\}$ such that $c \in b$.
+    Then there exists some $x \in A$ such that $b = \{x\} \times B$.
+    Therefore $c \in \{x\} \times B$.
+    But $x \in A$ meaning $c \in A \times B$ as well.
+
+  \paragraph{Conclusion}%
+
+    Since we have shown
+      $A \times B \subseteq \bigcup\; \{\{x\} \times B \mid x \in A\}$ and
+      $A \times B \supseteq \bigcup\; \{\{x\} \times B \mid x \in A\}$, it
+      follows \eqref{sub:exercise-5.5b-eq1} is a true identity.
 
 \end{proof}
 

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -1,8 +1,7 @@
 import Mathlib.Data.Set.Basic
-import Mathlib.SetTheory.ZFC.Basic
 
+import Common.Logic.Basic
 import Common.Set.Basic
-import Common.Set.OrderedPair
 
 /-! # Enderton.Chapter_3
 
@@ -11,13 +10,107 @@ Relations and Functions
 
 namespace Enderton.Set.Chapter_3
 
+/-! ## Ordered Pairs -/
+
 /--
+Kazimierz Kuratowski's definition of an ordered pair.
+-/
+def OrderedPair (x : α) (y : β) : Set (Set (α ⊕ β)) :=
+  {{Sum.inl x}, {Sum.inl x, Sum.inr y}}
+
+namespace OrderedPair
+
+/--
+For any sets `x`, `y`, `u`, and `v`, `⟨u, v⟩ = ⟨x, y⟩` **iff** `u = x ∧ v = y`.
+-/
+theorem ext_iff {x u : α} {y v : β}
+  : (OrderedPair x y = OrderedPair u v) ↔ (x = u ∧ y = v) := by
+  unfold OrderedPair
+  apply Iff.intro
+  · intro h
+    have hu := Set.ext_iff.mp h {Sum.inl u}
+    have huv := Set.ext_iff.mp h {Sum.inl u, Sum.inr v}
+    simp only [
+      Set.mem_singleton_iff,
+      Set.mem_insert_iff,
+      true_or,
+      iff_true
+    ] at hu
+    simp only [
+      Set.mem_singleton_iff,
+      Set.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 [Set.singleton_eq_singleton_iff] at hu_x
+        rw [hu_x] at huv_x
+        have hx_v := Set.pair_eq_singleton_mem_imp_eq_self huv_x
+        rw [hu_x, hx_v] at h
+        simp only [Set.mem_singleton_iff, Set.insert_eq_of_mem] at h
+        have := Set.pair_eq_singleton_mem_imp_eq_self $
+          Set.pair_eq_singleton_mem_imp_eq_self h
+        rw [← hx_v] at this
+        injection hu_x with p
+        injection this with q
+        exact ⟨p.symm, q⟩
+      · -- #### Case 2
+        -- `{u} = {x}` and `{u, v} = {x, y}`.
+        intro huv_xy hu_x
+        rw [Set.singleton_eq_singleton_iff] at hu_x
+        rw [hu_x] at huv_xy
+        by_cases hx_v : Sum.inl x = Sum.inr v
+        · rw [hx_v] at huv_xy
+          simp at huv_xy
+          have := Set.pair_eq_singleton_mem_imp_eq_self huv_xy.symm
+          injection hu_x with p
+          injection this with q
+          exact ⟨p.symm, q⟩
+        · rw [Set.ext_iff] at huv_xy
+          have := huv_xy (Sum.inr v)
+          simp at this
+          injection hu_x with p
+          exact ⟨p.symm, this.symm⟩
+    · apply Or.elim huv
+      · -- #### Case 3
+        -- `{u} = {x, y}` and `{u, v} = {x}`.
+        intro huv_x _
+        rw [Set.ext_iff] at huv_x
+        have hv_x := huv_x (Sum.inr v)
+        simp only [
+          Set.mem_singleton_iff,
+          Set.mem_insert_iff,
+          or_true,
+          true_iff
+        ] at hv_x
+      · -- #### Case 4
+        -- `{u} = {x, y}` and `{u, v} = {x, y}`.
+        intro _ hu_xy
+        rw [Set.ext_iff] at hu_xy
+        have hy_u := hu_xy (Sum.inr y)
+        simp only [
+          Set.mem_singleton_iff,
+          Set.mem_insert_iff,
+          or_true,
+          iff_true
+        ] at hy_u
+  · intro h
+    rw [h.left, h.right]
+
+end OrderedPair
+
+/-- ### Theorem 3B
+
 If `x ∈ C` and `y ∈ C`, then `⟨x, y⟩ ∈ 𝒫 𝒫 C`.
 -/
-theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
+theorem theorem_3b {C : Set (α ⊕ α)} (hx : Sum.inl x ∈ C) (hy : Sum.inr y ∈ C)
-  : Set.OrderedPair x y ∈ 𝒫 𝒫 C := by
+  : OrderedPair x y ∈ 𝒫 𝒫 C := by
-  have hxs : {x} ⊆ C := Set.singleton_subset_iff.mpr hx
+  have hxs : {Sum.inl x} ⊆ C := Set.singleton_subset_iff.mpr hx
-  have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
+  have hxys : {Sum.inl x, Sum.inr y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
   exact Set.mem_mem_imp_pair_subset hxs hxys
 
 /-- ### Exercise 5.1
@@ -25,7 +118,8 @@ theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
 Suppose that we attempted to generalize the Kuratowski definitions of ordered
 pairs to ordered triples by defining
 ```
-⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.
+⟨x, y, z⟩* = {{x}, {x, y}, {x, y, z}}.open Set
+
 ```
 Show that this definition is unsuccessful by giving examples of objects `u`,
 `v`, `w`, `x`, `y`, `z` with `⟨x, y, z⟩* = ⟨u, v, w⟩*` but with either `y ≠ v`
@@ -115,4 +209,53 @@ theorem exercise_5_3 {A : Set (Set α)} {𝓑 : Set (Set β)}
       · intro ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
         exact ⟨b, ⟨h₁, ⟨h₂, h₃⟩⟩⟩
 
+/-- ### Exercise 5.5a
+
+Assume that `A` and `B` are given sets, and show that there exists a set `C`
+such that for any `y`,
+```
+y ∈ C ↔ y = {x} × B for some x in A.
+```
+In other words, show that `{{x} × B | x ∈ A}` is a set.
+-/
+theorem exercise_5_5a {A : Set α} {B : Set β}
+  : ∃ C : Set (Set (α × β)),
+      y ∈ C ↔ ∃ x ∈ A, y = Set.prod {x} B := by
+  sorry
+
+/-- ### Exercise 5.5b
+
+With `A`, `B`, and `C` as above, show that `A × B = ∪ C`.
+-/
+theorem exercise_5_5b {A : Set α} (B : Set β)
+  : Set.prod A B = ⋃₀ {Set.prod ({x} : Set α) B | x ∈ A} := by
+  suffices Set.prod A B ⊆ ⋃₀ {Set.prod {x} B | x ∈ A} ∧
+           ⋃₀ {Set.prod {x} B | x ∈ A} ⊆ Set.prod A B from
+    Set.Subset.antisymm_iff.mpr this
+  apply And.intro
+  · show ∀ t, t ∈ Set.prod A B → t ∈ ⋃₀ {Set.prod {x} B | x ∈ A}
+    intro t h
+    simp only [Set.mem_setOf_eq] at h
+    unfold Set.sUnion sSup Set.instSupSetSet
+    simp only [Set.mem_setOf_eq, exists_exists_and_eq_and]
+    unfold Set.prod at h
+    simp only [Set.mem_setOf_eq] at h
+    refine ⟨t.fst, ⟨h.left, ?_⟩⟩
+    unfold Set.prod
+    simp only [Set.mem_singleton_iff, Set.mem_setOf_eq, true_and]
+    exact h.right
+  · show ∀ t, t ∈ ⋃₀ {Set.prod {x} B | x ∈ A} → t ∈ Set.prod A B
+    unfold Set.prod
+    intro t ht
+    simp only [
+      Set.mem_singleton_iff,
+      Set.mem_sUnion,
+      Set.mem_setOf_eq,
+      exists_exists_and_eq_and
+    ] at ht
+    have ⟨a, ⟨h, ⟨ha, hb⟩⟩⟩ := ht
+    simp only [Set.mem_setOf_eq]
+    rw [← ha] at h
+    exact ⟨h, hb⟩
+
 end Enderton.Set.Chapter_3

Common/Set.lean

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

Common/Set/OrderedPair.lean

@@ -1,98 +0,0 @@
-import Mathlib.Data.Set.Basic
-
-import Common.Logic.Basic
-import Common.Set.Basic
-
-namespace Set
-
-/--
-Kazimierz Kuratowski's definition of an ordered pair.
-
-Like `Set`, this is a homogeneous structure.
--/
-def OrderedPair (x y : α) : Set (Set α) := {{x}, {x, y}}
-
-namespace OrderedPair
-
-/--
-For any sets `x`, `y`, `u`, and `v`, `⟨u, v⟩ = ⟨x, y⟩` **iff** `u = x ∧ v = y`.
--/
-theorem ext_iff
-  : (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