diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index f9bed8a..b352a0f 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -2519,66 +2519,58 @@ Show that there is no set to which every ordered pair belongs. \end{proof} -\subsection{\unverified{Exercise 5.5a}}% +\subsection{\verified{Exercise 5.5a}}% \label{sub: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 \in C \iff y = \{x\} \times B \text{ for some } x \text{ in } A.$$ + \begin{equation} + \label{sub:exercise-5.5a-eq1} + y \in C \iff y = \{x\} \times B \text{ for some } x \text{ in } A. + \end{equation} In other words, show that $\{\{x\} \times B \mid x \in A\}$ is a set. \begin{proof} - Let $A$ and $B$ be arbitrary sets. - Also let $x \in A$. - By definition of the \nameref{sub:cartesian-product}, - \begin{equation} - \label{sub:exercise-5.5a-eq1} - \{x\} \times B = \{ \left< x, b \right> \mid b \in B \}. - \end{equation} - If $B = \emptyset$ then $\{x\} \times B$ trivially evaluates to the empty set, - which is a set by virtue of the \nameref{ref:empty-set-axiom}. - Therefore we continue under the assumption $B \neq \emptyset$. + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.exercise\_5\_5a} - We prove that (i) - $\{x\} \times B \subseteq \powerset{\powerset{(\{x\} \cup B)}}$ and then - (ii) that $\{x\} \times B$ 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. + Again by the \nameref{ref:pairing-axiom}, $\{\{a\} \times B\}$ is a set. - \paragraph{(i)}% - \label{par:exercise-5.5a-i} + Next, by another application of \nameref{sub:cartesian-product}, $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: + $$C = \{ y \in \powerset{(A \times B)} \mid + \exists a \in A, \forall x, \left[ x \in y \iff + \exists b \in B, x = \left< a, b \right> \right] \}.$$ + We now show that $C$ satisfies \eqref{sub:exercise-5.5a-eq1}. - Let $t \in \{x\} \times B$. - By \eqref{sub:exercise-5.5a-eq1} and definition of an - \nameref{ref:ordered-pair}, there exists a $b \in B$ such that - $$t = \left< x, b \right> = \{\{x\}, \{x, b\}\}.$$ - It trivially holds that - $$\{x\} \subseteq \{x\} \cup B \quad\text{and}\quad - \{x, b\} \subseteq \{x\} \cup B.$$ - Therefore, by definition of the \nameref{ref:power-set}, - $$\{x\} \in \powerset{(\{x\} \cup B)} \quad\text{and}\quad - \{x, b\} \in \powerset{(\{x\} \cup B)}.$$ - But then $\{\{x\}, \{x, b\}\} \subseteq \powerset{(\{x\} \cup B)}$. - Another application of the definition of the \nameref{ref:power-set} implies - that $$\{\{x\}, \{x, b\}\} \in \powerset{\powerset{(\{x\} \cup B)}}.$$ - Since this holds for all sets $t$, - $\{x\} \times B \subseteq \powerset{\powerset{(\{x\} \cup B)}}$. + \paragraph{($\Rightarrow$)}% - \paragraph{(ii)}% - \label{par:exercise-5.5a-ii} + Suppose $y \in C$. + Then there exists some $a \in A$ such that + $$\forall x, \left[ x \in y \iff + \exists b \in B, x = \left< a, b \right> \right].$$ + By the \nameref{ref:extensionality-axiom}, + \begin{align*} + y + & = \{ \left< a, b \right> \mid b \in B \} \\ + & = \{ \left< x, b \right> \mid x \in \{a\} \land b \in B \} \\ + & = \{ \{a\} \times B \}. + \end{align*} - By the \nameref{ref:subset-axioms}, there exists a set $C$ such that for any - set $y$, $$y \in C \iff - y \in \powerset{\powerset{(\{x\} \cup B)}} \land - (\exists b \in B, y = \left< x, b \right>).$$ - The above equation and \eqref{sub:exercise-5.5a-eq1} implies $C$ contains - only ordered pairs of the desired form. - By \nameref{par:exercise-5.5a-i}, $C$ contains them all. + \paragraph{($\Leftarrow$)}% - \paragraph{Conclusion}% - - Since $x$ was an arbitrarily chosen member of $A$, - \nameref{par:exercise-5.5a-ii} immediately implies that - $\{\{x\} \times B \mid x \in A\}$ is indeed a set. + Suppose $y = \{a\} \times B$ for some $a \in A$. + By \nameref{sub:cartesian-product}, $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>$. + This immediately proves $y \in C$. \end{proof} @@ -2633,4 +2625,87 @@ With $A$, $B$, and $C$ as above, show that $A \times B = \bigcup C$. \end{proof} +\section{Relations}% +\label{sec:relations} + +\subsection{\verified{Theorem 3D}}% +\label{sub:theorem-3d} + +\begin{theorem}[3D] + + If $\left< x, y \right> \in A$, then $x$ and $y$ belong to $\bigcup\bigcup A$. + +\end{theorem} + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Chapter\_3} + {Enderton.Set.Chapter\_3.theorem\_3d} + + Let $A$ be a set and $\left< x, y \right> \in A$. + By definition of an \nameref{ref:ordered-pair}, + $$\left< x, y \right> = \{\{x\}, \{x, y\}\}.$$ + By \nameref{sub:exercise-3.3}, $\{\{x\}, \{x, y\}\} \subseteq \bigcup A$. + Then $\{x, y\} \in \bigcup A$. + Another application of \nameref{sub:exercise-3.3} implies + $\{x, y\} \subseteq \bigcup\bigcup A$. + Therefore $x, y \in \bigcup\bigcup A$. + +\end{proof} + +\section{Exercises 6}% +\label{sec:exercises-6} + +\subsection{\unverified{Exercise 6.6}}% +\label{sub:exercise-6.6} + +Show that a set $A$ is a relation iff + $A \subseteq \textop{dom} A \times \textop{ran} A$. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\unverified{Exercise 6.7}}% +\label{sub:exercise-6.7} + +Show that if $R$ is a relation, then $\textop{fld} R = \bigcup\bigcup R$. + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\unverified{Exercise 6.8}}% +\label{sub:exercise-6.8} + +Show that for any set $\mathscr{A}$: + \begin{align*} + \textop{dom} \bigcup{\mathscr{A}} + & = \bigcup\; \{ \textop{dom} R \mid R \in \mathscr{A} \}, + \textop{ran} \bigcup{\mathscr{A}} + & = \bigcup\; \{ \textop{ran} R \mid R \in \mathscr{A} \}. + \end{align*} + +\begin{proof} + + TODO + +\end{proof} + +\subsection{\unverified{Exercise 6.9}}% +\label{sub:exercise-6.9} + +Discuss the result of replacing the union operation by the intersection + operation in the preceding problem. + +\begin{proof} + + TODO + +\end{proof} + \end{document} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 92f3154..e41790f 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1,5 +1,6 @@ import Mathlib.Data.Set.Basic +import Bookshelf.Enderton.Set.Chapter_2 import Common.Logic.Basic import Common.Set.Basic @@ -221,7 +222,61 @@ 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 + let C := {y ∈ 𝒫 (Set.prod A B) | ∃ a ∈ A, ∀ x, (x ∈ y ↔ ∃ b ∈ B, x = (a, b))} + refine ⟨C, ?_⟩ + apply Iff.intro + · intro hC + simp only [Set.mem_setOf_eq] at hC + have ⟨_, ⟨a, ⟨ha, h⟩⟩⟩ := hC + refine ⟨a, ⟨ha, ?_⟩⟩ + ext x + apply Iff.intro + · intro hxy + unfold Set.prod + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] + have ⟨b, ⟨hb, hx⟩⟩ := (h x).mp hxy + rw [Prod.ext_iff] at hx + simp only at hx + rw [← hx.right] at hb + exact ⟨hx.left, hb⟩ + · intro hx + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hx + have := (h (a, x.snd)).mpr ⟨x.snd, ⟨hx.right, rfl⟩⟩ + have hxab : x = (a, x.snd) := by + ext <;> simp + exact hx.left + rwa [← hxab] at this + · intro ⟨x, ⟨hx, hy⟩⟩ + show y ∈ 𝒫 Set.prod A B ∧ ∃ a, a ∈ A ∧ + ∀ (x : α × β), x ∈ y ↔ ∃ b, b ∈ B ∧ x = (a, b) + apply And.intro + · simp only [Set.mem_powerset_iff] + rw [hy] + unfold Set.prod + simp only [ + Set.mem_singleton_iff, + Set.setOf_subset_setOf, + and_imp, + Prod.forall + ] + intro a b ha hb + exact ⟨by rw [ha]; exact hx, hb⟩ + · refine ⟨x, ⟨hx, ?_⟩⟩ + intro p + apply Iff.intro + · intro hab + rw [hy] at hab + unfold Set.prod at hab + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] at hab + exact ⟨p.2, ⟨hab.right, by ext; exact hab.left; simp⟩⟩ + · intro ⟨b, ⟨hb, hab⟩⟩ + rw [hy] + unfold Set.prod + simp only [Set.mem_singleton_iff, Set.mem_setOf_eq] + rw [Prod.ext_iff] at hab + simp only at hab + rw [hab.right] + exact ⟨hab.left, hb⟩ /-- ### Exercise 5.5b @@ -258,4 +313,19 @@ theorem exercise_5_5b {A : Set α} (B : Set β) rw [← ha] at h exact ⟨h, hb⟩ +/-- ### Theorem 3D + +If `⟨x, y⟩ ∈ A`, then `x` and `y` belong to `⋃ ⋃ A`. +-/ +theorem theorem_3d {A : Set (Set (Set (α ⊕ α)))} (h : OrderedPair x y ∈ A) + : Sum.inl x ∈ ⋃₀ (⋃₀ A) ∧ Sum.inr y ∈ ⋃₀ (⋃₀ A) := by + have hp : OrderedPair x y ⊆ ⋃₀ A := Chapter_2.exercise_3_3 (OrderedPair x y) h + have hp' : ∀ t, t ∈ {{Sum.inl x}, {Sum.inl x, Sum.inr y}} → t ∈ ⋃₀ A := hp + + have hq := hp' {Sum.inl x, Sum.inr y} (by simp) + have hq' := Chapter_2.exercise_3_3 {Sum.inl x, Sum.inr y} hq + + have : ∀ t, t ∈ {Sum.inl x, Sum.inr y} → t ∈ ⋃₀ (⋃₀ A) := hq' + exact ⟨this (Sum.inl x) (by simp), this (Sum.inr y) (by simp)⟩ + end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/preamble.tex b/preamble.tex index 8e16cf5..46e8ea9 100644 --- a/preamble.tex +++ b/preamble.tex @@ -134,6 +134,7 @@ \newcommand{\ioc}[2]{\left(#1, #2\right]} \newcommand{\ioo}[2]{\left(#1, #2\right)} \newcommand{\powerset}[1]{\mathscr{P}#1} +\newcommand{\textop}[1]{\mathop{\text{#1}}} \newcommand{\ubar}[1]{\text{\b{$#1$}}} \let\oldemptyset\emptyset