From 993e9fe98119ea79bd58e157057dc430d308e14d Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Tue, 4 Jul 2023 13:13:57 -0600 Subject: [PATCH] Enderton. Exercise 3.31, Theorem 3K, and corollary. --- Bookshelf/Enderton/Set.tex | 144 +++++++++++++++++---- Bookshelf/Enderton/Set/Chapter_3.lean | 180 ++++++++++++++++++++++++++ 2 files changed, 296 insertions(+), 28 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index 35b0e91..bd5ddde 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/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} - Equality holds if $F$ is single-rooted. + 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 - $\exists u, \forall A \in \mathscr{A}, u \in A \land uFv$. + 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$. 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 - & = \bigcup\;\{G^{-1}[A] \mid A \in \mathscr{A}\}, + \img{G^{-1}}{\bigcup{\mathscr{A}}} + & = \bigcup\;\{\img{G^{-1}}{A} \mid A \in \mathscr{A}\}, \label{sub:corollary-3l-eq1} \\ - G^{-1}\left[\bigcap\mathscr{A}\right] - & = \bigcap\;\{G^{-1}[A] \mid A \in \mathscr{A}\} + \img{G^{-1}}{\bigcap{\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, - \nameref{ref:range}, and \nameref{sub:cartesian-product} of sets, - Then + By \nameref{sub:corollary-3c} and definition of the \nameref{ref:restriction}, + intersection, and \nameref{ref:range} of sets, \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} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 8495a7f..6b19d44 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/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 \ No newline at end of file