Enderton. Exercise 3.31, Theorem 3K, and corollary.

Bookshelf/Enderton/Set.tex

@@ -44,8 +44,18 @@ For any set $I$ and any function $H$ with domain $I$, if $H(i) \neq \emptyset$
 
 \end{axiom}
 
+\section{\pending{Cartesian Product}}%
+\label{ref:cartesian-product}
+
+Let $I$ be a set and let $H$ be a \nameref{ref:function} whose domain includes $I$.
+Then for each $i$ in $I$ we have the set $H(i)$.
+We define the \textbf{cartesian product} of the $H(i)$'s as
+  $$\bigtimes_{i \in I} H(i) = \{f \mid
+    f \text{ is a function with domain } I \text{ and }
+      (\forall i \in I) f(i) \in H(i)\}.$$
+
 \section{\defined{Compatible}}%
-\label{sec:compatible}
+\label{ref:compatible}
 
 A \nameref{ref:function} $F$ is \textbf{compatible} with relation $R$ if and
   only if for all $x$ and $y$ in $A$,
@@ -2569,9 +2579,8 @@ If not, then under what conditions does equality hold?
 
 \end{proof}
 
-\subsection{\verified{Cartesian Product}}%
+\subsection{\verified{Corollary 3C}}%
 \label{sub:corollary-3c}
-\label{sub:cartesian-product}
 
 \begin{theorem}[3C]
 
@@ -3018,7 +3027,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \end{proof}
 
-\subsection{\pending{Theorem 3K(a)}}%
+\subsection{\verified{Theorem 3K(a)}}%
 \label{sub:theorem-3k-a}
 
 \begin{theorem}[3K(a)]
@@ -3040,6 +3049,9 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3k\_a}
+
   Let $F$, $A$, $B$, and $\mathscr{A}$ be arbitrary sets.
   We prove (i) \eqref{sub:theorem-3k-a-eq1} and (ii)
     \eqref{sub:theorem-3k-a-eq2}.
@@ -3086,7 +3098,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \end{proof}
 
-\subsection{\pending{Theorem 3K(b)}}%
+\subsection{\verified{Theorem 3K(b)}}%
 \label{sub:theorem-3k-b}
 
 \begin{theorem}[3K(b)]
@@ -3103,13 +3115,23 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
       \img{F}{\bigcap\mathscr{A}} \subseteq
         \bigcap\;\{\img{F}{A} \mid A \in \mathscr{A}\}.
     \end{equation}
+    for nonempty $\mathscr{A}$.
   Equality holds if $F$ is single-rooted.
 
 \end{theorem}
 
 \begin{proof}
 
-  Let $F$, $A$, $B$, and $\mathscr{A}$ be arbitrary sets.
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3k\_b\_i}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3k\_b\_ii}
+
+  Let $F$, $A$, $B$ be arbitrary sets.
+  Let $\mathscr{A}$ be a nonempty set.
   We first prove (i) \eqref{sub:theorem-3k-b-eq1} and (ii)
     \eqref{sub:theorem-3k-b-eq2}.
   Then, assuming $F$ is single-rooted, we prove both (iii)
@@ -3162,14 +3184,14 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
     Then $\forall A \in \mathscr{A}, v \in \img{F}{A}$.
     By definition of the \nameref{ref:image} of a set,
       $\forall A \in \mathscr{A}, \exists u \in A, uFv$.
-    Since $F$ is single-rooted, it follows that
+    Since $F$ is single-rooted and $\mathscr{A}$ is nonempty, it follows that
-      $\exists u, \forall A \in \mathscr{A}, u \in A \land uFv$.
+      $\exists u, (\forall A \in \mathscr{A}, u \in A) \land uFv$.
     Equivalently, $\exists u \in \bigcap{A}, uFv$.
     Thus $v \in \img{F}{\bigcap{A}}$.
 
 \end{proof}
 
-\subsection{\pending{Theorem 3K(c)}}%
+\subsection{\verified{Theorem 3K(c)}}%
 \label{sub:theorem-3k-c}
 
 \begin{theorem}[3K(c)]
@@ -3186,6 +3208,14 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3k\_c\_i}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.theorem\_3k\_c\_ii}
+
   We prove that (i) \eqref{sub:theorem-3k-c-eq1} holds and (ii) equality holds
     if $F$ is single-rooted.
 
@@ -3219,21 +3249,21 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \end{proof}
 
-\subsection{\pending{Corollary 3L}}%
+\subsection{\verified{Corollary 3L}}%
 \label{sub:corollary-3l}
 
 \begin{theorem}[3L]
 
   For any function $G$ and sets $A$, $B$, and $\mathscr{A}$:
   \begin{align}
-    G^{-1}\left\llbracket\bigcup\mathscr{A}\right\rrbracket
+    \img{G^{-1}}{\bigcup{\mathscr{A}}}
-      & = \bigcup\;\{G^{-1}[A] \mid A \in \mathscr{A}\},
+      & = \bigcup\;\{\img{G^{-1}}{A} \mid A \in \mathscr{A}\},
       \label{sub:corollary-3l-eq1} \\
-    G^{-1}\left[\bigcap\mathscr{A}\right]
+    \img{G^{-1}}{\bigcap{\mathscr{A}}}
-      & = \bigcap\;\{G^{-1}[A] \mid A \in \mathscr{A}\}
+      & = \bigcap\;\{\img{G^{-1}}{A} \mid A \in \mathscr{A}\}
       \text{ for } \mathscr{A} \neq \emptyset,
       \label{sub:corollary-3l-eq2} \\
-    G^{-1}[A - B] & = G^{-1}[A] - G^{-1}[B].
+    \img{G^{-1}}{A - B} & = \img{G^{-1}}{A} - \img{G^{-1}}{B}.
       \label{sub:corollary-3l-eq3}
   \end{align}
 
@@ -3241,6 +3271,17 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
 
 \begin{proof}
 
+  \statementpadding
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.corollary\_3l\_i}
+
+  \lean*{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.corollary\_3l\_ii}
+
+  \lean{Bookshelf/Enderton/Set/Chapter\_3}
+    {Enderton.Set.Chapter\_3.corollary\_3l\_iii}
+
   \nameref{sub:theorem-3k-a} implies \eqref{sub:corollary-3l-eq1}.
   Because the inverse of a function is always single-rooted,
     \nameref{sub:theorem-3k-b} implies \eqref{sub:corollary-3l-eq2}.
@@ -3441,7 +3482,7 @@ Show that $A \times (B \cup C) = (A \times B) \cup (A \times C)$.
     {Enderton.Set.Chapter\_3.exercise\_3\_2a}
 
   Let $A$, $B$, and $C$ be arbitrary sets.
-  Then by definition of the \nameref{sub:cartesian-product} and union of sets,
+  Then by \nameref{sub:corollary-3c} and the definition of the union of sets,
     \begin{align*}
       A \times (B \cup C)
         & = \{ \left< x, y \right> \mid x \in A \land y \in (B \cup C) \} \\
@@ -3467,7 +3508,7 @@ Show that if $A \times B = A \times C$ and $A \neq \emptyset$, then $B = C$.
     {Enderton.Set.Chapter\_3.exercise\_3\_2b}
 
   Let $A$, $B$, and $C$ be arbitrary sets such that $A \neq \emptyset$.
-  By definition of the \nameref{sub:cartesian-product},
+  By \nameref{sub:corollary-3c},
     \begin{align}
       A \times B & = \{ \left< x, y \right> \mid x \in A \land y \in B \}
         & \label{sub:exercise-3.2b-eq1} \\
@@ -3513,7 +3554,7 @@ Show that $A \times \bigcup \mathscr{B} =
     {Enderton.Set.Chapter\_3.exercise\_3\_3}
 
   Let $A$ and $\mathscr{B}$ be arbitrary sets.
-  By definition of the \nameref{sub:cartesian-product} and the union of sets,
+  By \nameref{sub:corollary-3c} and the definition of the union of sets,
   \begin{align*}
     A \times \bigcup\mathscr{B}
       & = \{ \left< x, y \right> \mid
@@ -3564,10 +3605,10 @@ In other words, show that $\{\{x\} \times B \mid x \in A\}$ is a set.
 
   Let $a \in A$.
   By the \nameref{ref:pairing-axiom}, $\{a\}$ is a set.
-  By \nameref{sub:cartesian-product}, $\{a\} \times B$ is a set.
+  By \nameref{sub:corollary-3c}, $\{a\} \times B$ is a set.
   Again by the \nameref{ref:pairing-axiom}, $\{\{a\} \times B\}$ is a set.
 
-  Next, by another application of \nameref{sub:cartesian-product}, $A \times B$
+  Next, by another application of \nameref{sub:corollary-3c}, $A \times B$
     is a set.
   By the \nameref{ref:power-set-axiom}, $\powerset{(A \times B)}$ is a set.
   Thus, by the \nameref{ref:subset-axioms}, the following is also a set:
@@ -3593,7 +3634,7 @@ In other words, show that $\{\{x\} \times B \mid x \in A\}$ is a set.
   \paragraph{($\Leftarrow$)}%
 
     Suppose $y = \{a\} \times B$ for some $a \in A$.
-    By \nameref{sub:cartesian-product}, $x \in \{a\} \times B$ if and only if
+    By \nameref{sub:corollary-3c}, $x \in \{a\} \times B$ if and only if
       $\exists b \in B$ such that $x = \left< a, b \right>$.
     But then $x \in y$ if and only if $\exists b \in B$ such that
       $x = \left< a, b \right>$.
@@ -3618,7 +3659,7 @@ With $A$, $B$, and $C$ as above, show that $A \times B = \bigcup C$.
       A \times B = \bigcup\; \{\{x\} \times B \mid x \in A\}.
     \end{equation}
   The left-hand side of \eqref{sub:exercise-3.5b-eq1} is a set by virtue of
-    \nameref{sub:cartesian-product}.
+    \nameref{sub:corollary-3c}.
   The right-hand side of \eqref{sub:exercise-3.5b-eq1} is a set by virtue of
     \nameref{sub:exercise-3.5a}.
   We prove the set on each side is a subset of the other.
@@ -4193,9 +4234,8 @@ Show that $F \restriction A = F \cap (A \times \ran{F})$.
 \begin{proof}
 
   Let $F$ and $A$ be arbitrary sets.
-  By definition of the \nameref{ref:restriction}, intersection,
+  By \nameref{sub:corollary-3c} and definition of the \nameref{ref:restriction},
-    \nameref{ref:range}, and \nameref{sub:cartesian-product} of sets,
+    intersection, and \nameref{ref:range} of sets,
-  Then
     \begin{align*}
       F \restriction A
         & = \{\left< u, v \right> \mid uFv \land u \in A\} \\
@@ -4559,7 +4599,7 @@ Define
 
 \end{proof}
 
-\subsection{\sorry{Exercise 3.31}}%
+\subsection{\unverified{Exercise 3.31}}%
 \label{sub:exercise-3.31}
 
 Show that from the first form of the axiom of choice we can prove the second
@@ -4567,7 +4607,55 @@ Show that from the first form of the axiom of choice we can prove the second
 
 \begin{proof}
 
-  TODO
+  We prove the first form holds if and only if the second form holds.
+
+  \paragraph{($\Rightarrow$)}%
+
+    We assume the first form of the axiom of choice.
+    Let $I$ be a set and $H$ be a function with $\dom{H} = I$.
+    Furthermore, suppose $H(i) \neq \emptyset$ for all $i \in I$.
+    By definition of the \nameref{ref:cartesian-product},
+      $$\bigtimes_{i \in I} H(i) = \{f \mid
+        f \text{ is a function with } \dom{f} = I \text{ and }
+          (\forall i \in I) f(i) \in H(i)\}.$$
+    Consider the relation $R$ formed by
+      $$R = \bigcup_{i \in I} \{i\} \times H(i).$$
+    By the \nameref{ref:axiom-of-choice-1}, there exists a function
+      $f \subseteq R$ with $\dom{f} = I$.
+    Furthermore, for all $i \in I$, it must be $f(i) \in H(i)$ by construction.
+    Then $f$ is a member of $\bigtimes_{i \in I} H(i)$.
+    That is, $\bigtimes_{i \in I} H(i) \neq \emptyset$.
+
+  \paragraph{($\Leftarrow$)}%
+
+    We assume the second form of the axiom of choice.
+    Let $R$ be an arbitrary relation.
+    There are two cases to consider:
+
+    \subparagraph{Case 1}%
+
+      Suppose $\ran{R} = \emptyset$.
+      Then $R = \emptyset$.
+      Thus the function $\emptyset \subseteq R$ satisfies
+        $\dom{\emptyset} = \dom{R}$.
+
+    \subparagraph{Case 2}%
+
+      Suppose $\ran{R} \neq \emptyset$.
+      Let $I = \dom{R}$ and define $H \colon I \rightarrow \{\ran{R}\}$ as
+        $H(i) = \ran{R}$ for all $i \in I$.
+      By the \nameref{ref:axiom-of-choice-2},
+        $\bigtimes_{i \in I} H(i) \neq \emptyset$.
+      By definition of the \nameref{ref:cartesian-product}, there exists some
+        function $f$ such that $\dom{f} = I$ and
+        $(\forall i \in I) f(i) \in H(i) = \ran{R}$.
+      Thus $\dom{f} = \dom{R}$ and $f \subseteq R$ as desired.
+
+    \paragraph{Conclusion}%
+
+      The above cases are exhaustive and yield the same conclusion: for any
+        relation $R$ there exists a function $f \subseteq R$ such that
+        $\dom{f} = \dom{R}$.
 
 \end{proof}
 

Bookshelf/Enderton/Set/Chapter_3.lean

@@ -534,6 +534,186 @@ theorem theorem_3j_b {F : Set.Relation α} {A B : Set α}
         (∀ p ∈ F.comp H, p.1 = p.2)) ↔ F.mapsOnto A B := by
   sorry
 
+/-- #### Theorem 3K (a)
+
+The following hold for any sets. (`F` need not be a function.)
+The image of a union is the union of the images:
+```
+F⟦⋃ 𝓐⟧ = ⋃ {F⟦A⟧ | A ∈ 𝓐}
+```
+-/
+theorem theorem_3k_a {F : Set.Relation α} {𝓐 : Set (Set α)}
+  : F.image (⋃₀ 𝓐) = ⋃₀ { F.image A | A ∈ 𝓐 } := by
+  rw [Set.Subset.antisymm_iff]
+  apply And.intro
+  · show ∀ v, v ∈ F.image (⋃₀ 𝓐) → v ∈ ⋃₀ { F.image A | A ∈ 𝓐 }
+    intro v hv
+    unfold image at hv
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq] at hv
+    have ⟨u, hu⟩ := hv
+    have ⟨A, hA⟩ := hu.left
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq, exists_exists_and_eq_and]
+    refine ⟨A, hA.left, ?_⟩
+    show v ∈ F.image A
+    unfold image
+    simp only [Set.mem_setOf_eq]
+    exact ⟨u, hA.right, hu.right⟩
+  · show ∀ v, v ∈ ⋃₀ {x | ∃ A, A ∈ 𝓐 ∧ F.image A = x} → v ∈ F.image (⋃₀ 𝓐)
+    intro v hv
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq, exists_exists_and_eq_and] at hv
+    have ⟨A, hA⟩ := hv
+    unfold image at hA
+    simp only [Set.mem_setOf_eq] at hA
+    have ⟨u, hu⟩ := hA.right
+    unfold image
+    simp only [Set.mem_sUnion, Set.mem_setOf_eq]
+    exact ⟨u, ⟨A, hA.left, hu.left⟩, hu.right⟩
+
+/-! #### Theorem 3K (b)
+
+The following hold for any sets. (`F` need not be a function.)
+The image of an intersection is included in the intersection of the images:
+```
+F⟦⋂ 𝓐⟧ ⊆ ⋂ {F⟦A⟧ | A ∈ 𝓐}
+```
+Equality holds if `F` is single-rooted.
+-/
+
+theorem theorem_3k_b_i {F : Set.Relation α} {𝓐 : Set (Set α)}
+  : F.image (⋂₀ 𝓐) ⊆ ⋂₀ { F.image A | A ∈ 𝓐} := by
+  show ∀ v, v ∈ F.image (⋂₀ 𝓐) → v ∈ ⋂₀ { F.image A | A ∈ 𝓐}
+  intro v hv
+  unfold image at hv
+  simp only [Set.mem_sInter, Set.mem_setOf_eq] at hv
+  have ⟨u, hu⟩ := hv
+  simp only [
+    Set.mem_sInter,
+    Set.mem_setOf_eq,
+    forall_exists_index,
+    and_imp,
+    forall_apply_eq_imp_iff₂
+  ]
+  intro A hA
+  unfold image
+  simp only [Set.mem_setOf_eq]
+  exact ⟨u, hu.left A hA, hu.right⟩
+
+theorem theorem_3k_b_ii {F : Set.Relation α} {𝓐 : Set (Set α)}
+  (hF : F.isSingleRooted) (h𝓐 : Set.Nonempty 𝓐)
+  : F.image (⋂₀ 𝓐) = ⋂₀ { F.image A | A ∈ 𝓐} := by
+  rw [Set.Subset.antisymm_iff]
+  refine ⟨theorem_3k_b_i, ?_⟩
+  show ∀ v, v ∈ ⋂₀ {x | ∃ A, A ∈ 𝓐 ∧ image F A = x} → v ∈ image F (⋂₀ 𝓐)
+  intro v hv
+  simp only [
+    Set.mem_sInter,
+    Set.mem_setOf_eq,
+    forall_exists_index,
+    and_imp,
+    forall_apply_eq_imp_iff₂
+  ] at hv
+  unfold image at hv
+  simp only [Set.mem_setOf_eq] at hv
+  have ⟨u, hu⟩ : ∃ u, (∀ (a : Set α), a ∈ 𝓐 → u ∈ a) ∧ (u, v) ∈ F := by
+    have ⟨A, hA⟩ := h𝓐
+    have ⟨_, ⟨_, hv'⟩⟩ := hv A hA
+    have ⟨u, hu⟩ := hF v (mem_pair_imp_snd_mem_ran hv')
+    simp only [and_imp] at hu
+    refine ⟨u, ?_, hu.left.right⟩
+    intro a ha
+    have ⟨u₁, hu₁⟩ := hv a ha
+    have := hu.right u₁ (mem_pair_imp_fst_mem_dom hu₁.right) hu₁.right
+    rw [← this]
+    exact hu₁.left
+  unfold image
+  simp only [Set.mem_sInter, Set.mem_setOf_eq]
+  exact ⟨u, hu⟩
+
+/-! #### Theorem 3K (c)
+
+The following hold for any sets. (`F` need not be a function.)
+The image of a difference includes the difference of the images:
+```
+F⟦A⟧ - F⟦B⟧ ⊆ F⟦A - B⟧.
+```
+Equality holds if `F` is single-rooted.
+-/
+
+theorem theorem_3k_c_i {F : Set.Relation α} {A B : Set α}
+  : F.image A \ F.image B ⊆ F.image (A \ B) := by
+  show ∀ v, v ∈ F.image A \ F.image B → v ∈ F.image (A \ B)
+  intro v hv
+  have hv' : v ∈ image F A ∧ v ∉ image F B := hv
+  conv at hv' => arg 1; unfold image; simp only [Set.mem_setOf_eq, eq_iff_iff]
+  have ⟨u, hu⟩ := hv'.left
+  have hw : ∀ w ∈ B, (w, v) ∉ F := by
+    intro w hw nw
+    have nv := hv'.right
+    unfold image at nv
+    simp only [Set.mem_setOf_eq, not_exists, not_and] at nv
+    exact absurd nw (nv w hw)
+  have hu' : u ∉ B := by
+    by_contra nu
+    exact absurd hu.right (hw u nu)
+  unfold image
+  simp only [Set.mem_diff, Set.mem_setOf_eq]
+  exact ⟨u, ⟨hu.left, hu'⟩, hu.right⟩
+
+theorem theorem_3k_c_ii {F : Set.Relation α} {A B : Set α}
+  (hF : F.isSingleRooted)
+  : F.image A \ F.image B = F.image (A \ B) := by
+  rw [Set.Subset.antisymm_iff]
+  refine ⟨theorem_3k_c_i, ?_⟩
+  show ∀ v, v ∈ image F (A \ B) → v ∈ image F A \ image F B
+  intro v hv
+  unfold image at hv
+  simp only [Set.mem_diff, Set.mem_setOf_eq] at hv
+  have ⟨u, hu⟩ := hv
+  have hv₁ : v ∈ F.image A := by
+    unfold image
+    simp only [Set.mem_setOf_eq]
+    exact ⟨u, hu.left.left, hu.right⟩
+  have hv₂ : v ∉ F.image B := by
+    intro nv
+    unfold image at nv
+    simp only [Set.mem_setOf_eq] at nv
+    have ⟨u₁, hu₁⟩ := nv
+    have ⟨x, hx⟩ := hF v (mem_pair_imp_snd_mem_ran hu.right)
+    simp only [and_imp] at hx
+    have hr₁ := hx.right u (mem_pair_imp_fst_mem_dom hu.right) hu.right
+    have hr₂ := hx.right u₁ (mem_pair_imp_fst_mem_dom hu₁.right) hu₁.right
+    rw [hr₂, ← hr₁] at hu₁
+    exact absurd hu₁.left hu.left.right
+  exact ⟨hv₁, hv₂⟩
+
+/-! #### Corollary 3L
+
+For any function `G` and sets `A`, `B`, and `𝓐`:
+
+```
+G⁻¹⟦⋃ 𝓐⟧ = ⋃ {G⁻¹⟦A⟧ | A ∈ 𝓐},
+G⁻¹⟦𝓐⟧ = ⋂ {G⁻¹⟦A⟧ | A ∈ 𝓐} for 𝓐 ≠ ∅,
+G⁻¹⟦A - B⟧ = G⁻¹⟦A⟧ - G⁻¹⟦B⟧.
+```
+-/
+
+theorem corollary_3l_i {G : Set.Relation α} {𝓐 : Set (Set α)}
+  : G.inv.image (⋃₀ 𝓐) = ⋃₀ {G.inv.image A | A ∈ 𝓐} := theorem_3k_a
+
+theorem corollary_3l_ii {G : Set.Relation α} {𝓐 : Set (Set α)}
+  (hG : G.isSingleValued) (h𝓐 : Set.Nonempty 𝓐)
+  : G.inv.image (⋂₀ 𝓐) = ⋂₀ {G.inv.image A | A ∈ 𝓐} := by
+  have hG' : G.inv.isSingleRooted :=
+    single_valued_self_iff_single_rooted_inv.mp hG
+  exact theorem_3k_b_ii hG' h𝓐
+
+theorem corollary_3l_iii {G : Set.Relation α} {A B : Set α}
+  (hG : G.isSingleValued)
+  : G.inv.image (A \ B) = G.inv.image A \ G.inv.image B := by
+  have hG' : G.inv.isSingleRooted :=
+    single_valued_self_iff_single_rooted_inv.mp hG
+  exact (theorem_3k_c_ii hG').symm
+
 end
 
 end Enderton.Set.Chapter_3