Enderton. Exercise 5.(1|2a|2b).

Bookshelf/Enderton/Set.tex

@@ -2363,4 +2363,114 @@ If not, then under what conditions does equality hold?
 
 \end{proof}
 
+\section{Exercises 5}%
+\label{sec:exercises-5}
+
+\subsection{\verified{Exercise 5.1}}%
+\label{sub:exercise-5.1}
+
+Suppose that we attempted to generalize the Kuratowski definitions of ordered
+  pairs to ordered triples by defining
+  $$\left< x, y, z \right>^* = \{\{x\}, \{x, y\}, \{x, y, z\}\}.$$
+Show that this definition is unsuccessful by giving examples of objects
+  $u$, $v$, $w$, $x$, $y$, $z$ with
+  $\left< x, y, z \right>^* = \left< u, v, w \right>^*$ but with either
+  $y \neq v$ or $z \neq w$ (or both).
+
+\begin{proof}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_5\_1}
+
+  Let $x = 1$, $y = 1$, and $z = 2$.
+  Let $u = 1$, $v = 2$, and $w = 2$.
+  Then
+    \begin{align*}
+      \left< x, y, z \right>^*
+        & = \{\{x\}, \{x, y\}, \{x, y, z\}\} \\
+        & = \{\{1\}, \{1, 1\}, \{1, 1, 2\}\} \\
+        & = \{\{1\}, \{1, 2\}\}.
+    \end{align*}
+  Likewise
+    \begin{align*}
+      \left< u, v, w \right>^*
+        & = \{\{u\}, \{u, v\}, \{u, v, w\}\} \\
+        & = \{\{1\}, \{1, 2\}, \{1, 2, 2\}\} \\
+        & = \{\{1\}, \{1, 2\}\}.
+    \end{align*}
+  Thus $\left< x, y, z \right>^* = \left< u, v, w \right>^*$ but $y \neq v$.
+
+\end{proof}
+
+\subsection{\verified{Exercise 5.2a}}%
+\label{sub:exercise-5.2a}
+
+Show that $A \times (B \cup C) = (A \times B) \cup (A \times C)$.
+
+\begin{proof}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_5\_2a}
+
+  Let $A$, $B$, and $C$ be arbitrary sets.
+  Then by definition of the \nameref{sub:cartesian-product} and union of sets,
+    \begin{align*}
+      A \times (B \cup C)
+        & = \{ \left< x, y \right> \mid x \in A \land y \in (B \cup C) \} \\
+        & = \{ \left< x, y \right> \mid
+          x \in A \land (y \in B \lor y \in C) \} \\
+        & = \{ \left< x, y \right> \mid
+          (x \in A \land y \in B) \lor (x \in A \land y \in C) \} \\
+        & = \{ \left< x, y \right> \mid (x \in A \land y \in B) \} \cup
+          \{ \left< x, y \right> \mid (x \in A \land y \in C) \} \\
+        & = (A \times B) \cup (A \times C).
+    \end{align*}
+
+\end{proof}
+
+\subsection{\verified{Exercise 5.2b}}%
+\label{sub:exercise-5.2b}
+
+Show that if $A \times B = A \times C$ and $A \neq \emptyset$, then $B = C$.
+
+\begin{proof}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.exercise\_5\_2b}
+
+  Let $A$, $B$, and $C$ be arbitrary sets such that $A \neq \emptyset$.
+  By definition of the \nameref{sub:cartesian-product},
+    \begin{align}
+      A \times B & = \{ \left< x, y \right> \mid x \in A \land y \in B \}
+        & \label{sub:exercise-5.2b-eq1} \\
+      A \times C & = \{ \left< x, y \right> \mid x \in A \land y \in C \}.
+        & \label{sub:exercise-5.2b-eq2}
+    \end{align}
+  There are two cases to consider:
+
+  \paragraph{Case 1}%
+
+    Suppose $B \neq \emptyset$.
+    Then $A \times B \neq \emptyset$ and $A \times C \neq \emptyset$.
+    Let $\left< x, y \right> \in A \times B$.
+    By \eqref{sub:exercise-5.2b-eq1}, $x \in A$ and $y \in B$.
+    By the \nameref{ref:extensionality-axiom},
+      $$\left< x, y \right> \in A \times B \iff \left< x, y \right> \in A \times C.$$
+    Therefore $\left< x, y \right> \in A \times C$.
+    By \eqref{sub:exercise-5.2b-eq2}, $x \in A$ and $y \in C$.
+    Since membership of $y$ in $B$ and in $C$ holds biconditionally, the
+      \nameref{ref:extensionality-axiom} indicates $B = C$.
+
+  \paragraph{Case 2}%
+
+    Suppose $B = \emptyset$.
+    Then there is no $\left< x, y \right>$ such that $x \in A$ and $y \in B$.
+    Thus $A \times B = \emptyset$ and $A \times C = \emptyset$.
+    But then there cannot exist an $\left< x, y \right>$ such that $x \in A$
+      and $y \in C$ either.
+    Since $A \neq \emptyset$, it must be the case that $C = \emptyset$.
+    Thus $B = C$.
+
+\end{proof}
+
 \end{document}

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -1,6 +1,7 @@
 import Mathlib.Data.Set.Basic
 import Mathlib.SetTheory.ZFC.Basic
 
+import Common.Set.Basic
 import Common.Set.OrderedPair
 
 /-! # Enderton.Chapter_3
@@ -19,4 +20,71 @@ theorem theorem_3b {C : Set α} (hx : x ∈ C) (hy : y ∈ C)
   have hxys : {x, y} ⊆ C := Set.mem_mem_imp_pair_subset hx hy
   exact Set.mem_mem_imp_pair_subset hxs hxys
 
+/-- ### Exercise 5.1
+
+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}}.
+```
+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`
+or `z ≠ w` (or both).
+-/
+theorem exercise_5_1 {x y z u v w : ℕ}
+  (hx : x = 1) (hy : y = 1) (hz : z = 2)
+  (hu : u = 1) (hv : v = 2) (hw : w = 2)
+  : ({{x}, {x, y}, {x, y, z}} : Set (Set ℕ)) = {{u}, {u, v}, {u, v, w}}
+  ∧ y ≠ v := by
+  apply And.intro
+  · rw [hx, hy, hz, hu, hv, hw]
+    simp
+  · rw [hy, hv]
+    simp only
+
+/-- ### Exercise 5.2a
+
+Show that `A × (B ∪ C) = (A × B) ∪ (A × C)`.
+-/
+theorem exercise_5_2a {A B C : Set α}
+  : Set.prod A (B ∪ C) = (Set.prod A B) ∪ (Set.prod A C) := by
+  calc Set.prod A (B ∪ C)
+    _ = { p | p.1 ∈ A ∧ p.2 ∈ B ∪ C } := rfl
+    _ = { p | p.1 ∈ A ∧ (p.2 ∈ B ∨ p.2 ∈ C) } := rfl
+    _ = { p | (p.1 ∈ A ∧ p.2 ∈ B) ∨ (p.1 ∈ A ∧ p.2 ∈ C) } := by
+      ext x
+      rw [Set.mem_setOf_eq]
+      conv => lhs; rw [and_or_left]
+    _ = { p | p ∈ Set.prod A B ∨ (p ∈ Set.prod A C) } := rfl
+    _ = (Set.prod A B) ∪ (Set.prod A C) := rfl
+
+/-- ### Exercise 5.2b
+
+Show that if `A × B = A × C` and `A ≠ ∅`, then `B = C`.
+-/
+theorem exercise_5_2b {A B C : Set α}
+  (h : Set.prod A B = Set.prod A C) (hA : Set.Nonempty A)
+  : B = C := by
+  by_cases hB : Set.Nonempty B
+  · suffices B ⊆ C ∧ C ⊆ B from Set.Subset.antisymm_iff.mpr this
+    have ⟨a, ha⟩ := hA
+    apply And.intro
+    · show ∀ t, t ∈ B → t ∈ C
+      intro t ht
+      have : (a, t) ∈ Set.prod A B := ⟨ha, ht⟩
+      rw [h] at this
+      exact this.right
+    · show ∀ t, t ∈ C → t ∈ B
+      intro t ht
+      have : (a, t) ∈ Set.prod A C := ⟨ha, ht⟩
+      rw [← h] at this
+      exact this.right
+  · have nB : B = ∅ := Set.not_nonempty_iff_eq_empty.mp hB
+    rw [nB, Set.prod_right_emptyset_eq_emptyset, Set.ext_iff] at h
+    rw [nB]
+    by_contra nC
+    have ⟨a, ha⟩ := hA
+    have ⟨c, hc⟩ := Set.nonempty_iff_ne_empty.mpr (Ne.symm nC)
+    exact (h (a, c)).mpr ⟨ha, hc⟩
+
 end Enderton.Set.Chapter_3

Common/Set/Basic.lean

@@ -1,4 +1,5 @@
 import Mathlib.Data.Set.Basic
+import Mathlib.SetTheory.ZFC.Basic
 
 import Common.Logic.Basic
 
@@ -128,6 +129,42 @@ Every `Set` is a member of its own powerset.
 theorem self_mem_powerset_self {A : Set α}
   : A ∈ 𝒫 A := subset_self A
 
+/-! ## Cartesian Product -/
+
+/--
+For any `Set` `A`, `∅ × A = ∅`.
+-/
+theorem prod_left_emptyset_eq_emptyset {A : Set α}
+  : Set.prod (∅ : Set α) A = ∅ := by
+  unfold prod
+  simp only [mem_empty_iff_false, false_and, setOf_false]
+
+/--
+For any `Set` `A`, `A × ∅ = ∅`.
+-/
+theorem prod_right_emptyset_eq_emptyset {A : Set α}
+  : Set.prod A (∅ : Set α) = ∅ := by
+  unfold prod
+  simp only [mem_empty_iff_false, and_false, setOf_false]
+
+/--
+For any `Set`s `A` and `B`, if both `A` and `B` are nonempty, then `A × B` is
+also nonempty.
+-/
+theorem prod_nonempty_nonempty_imp_nonempty_prod {A B : Set α}
+  : A ≠ ∅ ∧ B ≠ ∅ ↔ Set.prod A B ≠ ∅ := by
+  apply Iff.intro
+  · intro nAB h
+    have ⟨a, ha⟩ := nonempty_iff_ne_empty.mpr nAB.left
+    have ⟨b, hb⟩ := nonempty_iff_ne_empty.mpr nAB.right
+    rw [Set.ext_iff] at h
+    exact (h (a, b)).mp ⟨ha, hb⟩
+  · intro h
+    rw [← nonempty_iff_ne_empty] at h
+    have ⟨(a, b), ⟨ha, hb⟩⟩ := h
+    rw [← nonempty_iff_ne_empty, ← nonempty_iff_ne_empty]
+    exact ⟨⟨a, ha⟩, ⟨b, hb⟩⟩
+
 /-! ## Symmetric Difference -/
 
 /--