From 98ecc12995b13f6203a4e3b15c3faa08cd011743 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 8 Jul 2023 10:01:43 -0600 Subject: [PATCH] Enderton. Additional equivalence relation exercises. --- Bookshelf/Enderton/Set.tex | 352 +++++++++++++++++++++--- Bookshelf/Enderton/Set/Chapter_3.lean | 380 ++++++++++++++++++++++++-- Bookshelf/Enderton/Set/Relation.lean | 46 ++++ Common/Logic/Basic.lean | 11 + 4 files changed, 734 insertions(+), 55 deletions(-) diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex index f1eee7d..428c543 100644 --- a/Bookshelf/Enderton/Set.tex +++ b/Bookshelf/Enderton/Set.tex @@ -3298,7 +3298,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \section{Equivalence Relations}% \label{sec:equivalence-relations} -\subsection{\pending{Theorem 3M}}% +\subsection{\verified{Theorem 3M}}% \label{sub:theorem-3m} \begin{theorem}[3M] @@ -3310,6 +3310,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\_3m} + Suppose $R$ is a \nameref{ref:symmetric} and \nameref{ref:transitive} \nameref{ref:relation}. By definition, the \nameref{ref:field} of $R$ is given by @@ -3331,7 +3334,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} -\subsection{\pending{Lemma 3N}}% +\subsection{\verified{Lemma 3N}}% \label{sub:lemma-3n} \begin{lemma}[3N] @@ -3344,6 +3347,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.lemma\_3n} + Suppose $R$ is an \nameref{ref:equivalence-relation} on set $A$. Let $x, y \in A$. @@ -3377,7 +3383,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} -\subsection{\pending{Theorem 3P}}% +\subsection{\verified{Theorem 3P}}% \label{sub:theorem-3p} \begin{theorem}[3P] @@ -3390,12 +3396,23 @@ 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\_3p} + Let $\Pi = \{[x]_R \mid x \in A\}$. - We show that (i) no two different sets in $\Pi$ have any common elements and - (ii) that each element of $A$ is in some set in $\Pi$. + We show that (i) there are no empty sets in $\Pi$, (ii) no two different sets + in $\Pi$ have any common elements and (iii) that each element of $A$ is in + some set in $\Pi$. \paragraph{(i)}% + By construction, every element of $\Pi$ is of form $[x]_R$ for some + $x \in A$. + At the very least, $x \in A$ is also in $[x]_R$. + Thus every element of $\Pi$ must be nonempty. + + \paragraph{(ii)}% + Let $[x]_R, [y]_R \in \Pi$ be two different sets. We must show that $[x]_R \cap [y]_R = \emptyset$. For the sake of contradiction, suppose $[x]_R \cap [y]_R \neq \emptyset$. @@ -3408,7 +3425,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. contradicting the distinctness of $[x]_R$ and $[y]_R$. Thus it follows $[x]_R \cap [y]_R] = \emptyset$. - \paragraph{(ii)}% + \paragraph{(iii)}% Let $x \in A$. Since $R$ is an \nameref{ref:equivalence-relation} on $A$, it follows @@ -3417,7 +3434,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. \end{proof} -\subsection{\sorry{Theorem 3Q}}% +\subsection{\pending{Theorem 3Q}}% \label{sub:theorem-3q} \begin{theorem}[3Q] @@ -3426,15 +3443,47 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one. $F \colon A \rightarrow A$. If $F$ is compatible with $R$, then there exists a unique $\hat{F} \colon A / R \rightarrow A / R$ such that - $$\hat{F}([x]_R) = [F(x)]_R \quad\text{for all } x \text{ in } A.$$ + \begin{equation} + \label{sub:theorem-3q-eq1} + \hat{F}([x]_R) = [F(x)]_R \quad\text{for all } x \text{ in } A. + \end{equation} If $F$ is not compatible with $R$, then no such $\hat{F}$ exists. - Analogous results apply to functions from $A \times A$ into $A$. \end{theorem} \begin{proof} - TODO + Let $R$ be an \nameref{ref:equivalence-relation} on $A$ and + $F \colon A \rightarrow A$. + Suppose $F$ is \nameref{ref:compatible} with $R$. + Next define \nameref{ref:relation} $\hat{F}$ to be + $$\hat{F} = \{([x]_R, [F(x)]_R) \mid x \in A\}.$$ + + By construction $\hat{F}$ has domain $A / R$ and + $\ran{\hat{F}} \subseteq A / R$. + All that remains is proving $\hat{F}$ is single-valued. + Let $[x_1]_R, [x_2]_R \in \dom{\hat{F}}$ such that $[x_1]_R = [x_2]_R$. + By definition of $\hat{F}$, $\left< [x_1]_R, [F(x_1)]_R \right> \in \hat{F}$ + and $\left< [x_2]_R, [F(x_2)]_R \right> \in \hat{F}$. + By \nameref{sub:lemma-3n}, $[x_1]_R = [x_2]_R$ implies $x_1Rx_2$. + Since $F$ is compatible, $F(x_1)RF(x_2)$. + Another application of \nameref{sub:lemma-3n} implies that + $[F(x_1)]_R = [F(x_2)]_R$. + Thus $\hat{F}$ is be single-valued. + + Uniqueness follows immediately from the \nameref{ref:extensionality-axiom}. + + \suitdivider + + Suppose $F$ is not compatible with $R$. + Then there exists some $x, y \in A$ such that $xRy$ and $\neg F(x)RF(y)$. + By \nameref{sub:lemma-3n}, $[x]_R = [y]_R$. + For the sake of contradiction, suppose a function $\hat{F}$ exists satisfying + \eqref{sub:theorem-3q-eq1}. + Then $\hat{F}([x]_R) = \hat{F}([y]_R)$ and $[F(x)]_R = [F(y)]_R$. + Then \nameref{sub:lemma-3n} implies $F(x)RF(y)$, a contradiction. + Therefore our original hypothesis must be incorrect. + That is, there is no function $\hat{F}$ satisfying \eqref{sub:theorem-3q-eq1}. \end{proof} @@ -4802,32 +4851,149 @@ Show that from the first form of the axiom of choice we can prove the second \end{proof} -\subsection{\sorry{Exercise 3.32}}% -\label{sub:exercise-3.32} +\subsection{\verified{Exercise 3.32a}}% +\label{sub:exercise-3.32-a} -\begin{enumerate}[(a)] - \item Show that $R$ is symmetric iff $R^{-1} \subseteq R$. - \item Show that $R$ is transitive iff $R \circ R \subseteq R$. -\end{enumerate} +Show that $R$ is symmetric iff $R^{-1} \subseteq R$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_32\_a} + + \paragraph{($\Rightarrow$)}% + + Suppose $R$ is \nameref{ref:symmetric}. + Let $\left< x, y \right> \in R^{-1}$. + By definition of the \nameref{ref:inverse} of a set, + $\left< y, x \right> \in R$. + By symmetry, $\left< x, y \right> \in R$. + Thus $R^{-1} \subseteq R$. + + \paragraph{($\Leftarrow$)}% + + Suppose $R^{-1} \subseteq R$. + Let $\left< x, y \right> \in R$. + By definition of the \nameref{ref:inverse} of a set, + $\left< y, x \right> \in R^{-1}$. + Since $R^{-1} \subseteq R$, $\left< y, x \right> \in R$. + Therefore $\left< x, y \right>$ and $\left< y, x \right>$ are both in $R$. + In other words, $R$ is symmetric. \end{proof} -\subsection{\sorry{Exercise 3.33}}% +\subsection{\verified{Exercise 3.32b}}% +\label{sub:exercise-3.32-b} + +Show that $R$ is transitive iff $R \circ R \subseteq R$. + +\begin{proof} + + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_32\_b} + + \paragraph{($\Rightarrow$)}% + + Suppose $R$ is \nameref{ref:transitive}. + Let $\left< x, y \right> \in R \circ R$. + By definition of the \nameref{ref:composition} of a set, + there exists some $t$ such that $xRt \land tRy$. + That is, $\left< x, t \right> \in R$ and $\left< t, y \right> \in R$. + Since $R$ is transitive, it follows $\left< x, y \right> \in R$. + + \paragraph{($\Leftarrow$)}% + + Suppose $R \circ R \subseteq R$. + Let $\left< x, y \right>, \left< y, z \right> \in R$. + By definition of the \nameref{ref:composition} of a set, + $$R \circ R = \{\left< u, v \right> \mid \exists t(uRt \land tRv)\}.$$ + Then $\left< x, z \right> \in R \circ R$. + Since $R \circ R \subseteq R$, it follows $\left< x, z \right> \in R$. + Thus $R$ is transitive. + +\end{proof} + +\subsection{\verified{Exercise 3.33}}% \label{sub:exercise-3.33} Show that $R$ is a symmetric and transitive relation iff $R = R^{-1} \circ R$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_33} + + By definition of the \nameref{ref:inverse} and \nameref{ref:composition} + of sets, + \begin{align} + R^{-1} \circ R + & = \{ (u, v) \mid \exists t(uRt \land tR^{-1}v) \} + \nonumber \\ + & = \{ (u, v) \mid \exists t(uRt \land vRt) \}. + \label{sub:exercise-3.33-eq1} + \end{align} + + \paragraph{($\Rightarrow$)}% + + Suppose $R$ is symmetric and transitive. + We now show that $R \subseteq R^{-1} \circ R$ and + $R^{-1} \circ R \subseteq R$. + + \subparagraph{($\subseteq$)}% + + Let $\left< x, y \right> \in R$. + Since $R$ is symmetric, $\left< y, x \right> \in R$. + Since $R$ is transitive, $\left< x, x \right> \in R$. + Then there exists a $t$ such that $\left< x, t \right> \in R$ and + $\left< y, t \right> \in R$, namely $t = x$. + By \eqref{sub:exercise-3.33-eq1}, + $\left< x, y \right> \in R^{-1} \circ R$. + + \subparagraph{($\supseteq$)}% + + Let $\left< x, y \right> \in R^{-1} \circ R$. + By \eqref{sub:exercise-3.33-eq1}, there exists some $t$ such that + $\left< x, t \right> \in R$ and $\left< y, t \right> \in R$. + But $R$ is symmetric meaning $\left< t, y \right> \in R$. + Since $R$ is transitive, it follows $\left< x, y \right> \in R$. + + \paragraph{($\Leftarrow$)}% + + Suppose $R = R^{-1} \circ R$. + We prove that (i) $R$ is symmetric and (ii) $R$ is transitive. + + \subparagraph{(i)}% + \label{spar:exercise-3.33-i} + + First we note that $R$ is equal to its inverse: + \begin{align} + R^{-1} + & = (R^{-1} \circ R)^{-1} \nonumber \\ + & = R^{-1} \circ (R^{-1})^{-1} + & \textref{sub:theorem-3i} \nonumber \\ + & = R^{-1} \circ R + & \textref{sub:theorem-3e} \nonumber \\ + & = R \label{sub:exercise-3.33-eq2}. + \end{align} + Now let $\left< x, y \right> \in R$. + By \eqref{sub:exercise-3.33-eq2} $\left< x, y \right> \in R^{-1}$. + By definition of the \nameref{ref:inverse} of a set, + $\left< y, x \right> \in R$. + Thus $R$ is symmetric. + + \subparagraph{(ii)}% + + Let $\left< x, y \right>, \left< y, z \right> \in R$. + By \nameref{spar:exercise-3.33-i}, $R$ is symmetric. + Thus $\left< z, y \right> \in R$. + By \eqref{sub:exercise-3.33-eq1}, it follows + $\left< x, z \right> \in R^{-1} \circ R$. + Since $R^{-1} \circ R = R$, it follows $\left< x, z \right> \in R$. + Thus $R$ is transitive. \end{proof} -\subsection{\sorry{Exercise 3.34}}% +\subsection{\verified{Exercise 3.34}}% \label{sub:exercise-3.34} Assume that $\mathscr{A}$ is a nonempty set, every member of which is a @@ -4840,63 +5006,185 @@ Assume that $\mathscr{A}$ is a nonempty set, every member of which is a \begin{proof} - TODO + \statementpadding + + \lean*{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_34\_a} + + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_34\_b} + + \paragraph{(a)}% + + Because $\mathscr{A} \neq \emptyset$, $\bigcap{\mathscr{A}}$ is + well-defined. + We prove that $\bigcap{\mathscr{A}}$ is a transitive relation. + Let $\left< x, y \right>, \left< y, z \right> \in \bigcap{\mathscr{A}}$. + Then forall $A$ in $\mathscr{A}$, it follows + $\left< x, y \right>, \left< y, z \right> \in A$. + Since $A$ is transitive, it follows $\left< x, z \right> \in A$. + Since this holds for all $A \in \mathscr{A}$, it follows that + $\left< x, z \right> \in A$ as well. + Thus $\bigcap{\mathscr{A}}$ is transitive. + + \paragraph{(b)}% + + We show that $\bigcup{\mathscr{A}}$ is not necessarily transitive with a + counterexample. + Suppose $$\mathscr{A} = \{ + \{\left< 1, 2 \right>, \left< 2, 3 \right>, \left< 1, 3 \right>\}, + \{\left< 2, 1 \right>\} + \}.$$ + Notice that the two members of $\mathscr{A}$ are transitive relations. + Now $$\bigcup{\mathscr{A}} = \{ + \left< 1, 2 \right>, + \left< 2, 3 \right>, + \left< 1, 3 \right>, + \left< 2, 1 \right>, + \}.$$ + But the above cannot be transitive, for $\left< 1, 2 \right>$ and + $\left< 2, 1 \right>$ are members of the set, but $\left< 1, 1 \right>$ + is not. \end{proof} -\subsection{\sorry{Exercise 3.35}}% +\subsection{\verified{Exercise 3.35}}% \label{sub:exercise-3.35} Show that for any $R$ and $x$, we have $[x]_R = \img{R}{\{x\}}$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_35} + + Let $R$ and $x$ be arbitrary sets. + Then + \begin{align*} + [x]_R + & = \{t \mid xRt\} \\ + & = \{t \mid (\exists u \in \{x\})uRt\} \\ + & = \img{R}{\{x\}}. + \end{align*} \end{proof} -\subsection{\sorry{Exercise 3.36}}% +\subsection{\verified{Exercise 3.36}}% \label{sub:exercise-3.36} Assume that $f \colon A \rightarrow B$ and that $R$ is an equivalence relation on $B$. Define $Q$ to be the set - $$\{\left< x, y \right> \in A \times A \mid - \left< f(x), f(x) \right> \in R\}.$$ + \begin{equation} + \label{sub:exercise-3.36-eq1} + \{\left< x, y \right> \in A \times A \mid + \left< f(x), f(y) \right> \in R\}. + \end{equation} Show that $Q$ is an equivalence relation on $A$. \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_36} + + We prove that (i) $Q$ is reflexive on $A$, (ii) $Q$ is symmetric, and (iii) + $Q$ is transitive. + + \paragraph{(i)}% + + Let $x \in A$. + By hypothesis, $f(x) \in B$. + Since $R$ is an equivalence relation on $B$, $R$ is reflexive on $B$. + Thus $\left< f(x), f(x) \right> \in R$. + But then \eqref{sub:exercise-3.36-eq1} implies $\left< x, x \right> \in Q$. + Thus $Q$ is reflexive on $A$. + + \paragraph{(ii)}% + + Let $\left< x, y \right> \in Q$. + By \eqref{sub:exercise-3.36-eq1}, $\left< f(x), f(y) \right> \in R$. + Since $R$ is an equivalence relation on $B$, $R$ is symmetric. + Thus $\left< f(y), f(x) \right> \in R$. + But then \eqref{sub:exercise-3.36-eq1} implies $\left< y, x \right> \in Q$. + Thus $Q$ is symmetric. + + \paragraph{(iii)}% + + Let $\left< x, y \right>, \left< y, z \right> \in Q$. + By \eqref{sub:exercise-3.36-eq1}, + $\left< f(x), f(y) \right>, \left< f(y), f(z) \right> \in R$. + Since $R$ is an equivalence relation on $B$, $R$ is transitive. + Thus $\left< f(x), f(z) \right> \in R$. + But then \eqref{sub:exercise-3.36-eq1} implies $\left< x, z \right> \in Q$. + Thus $Q$ is transitive. \end{proof} -\subsection{\sorry{Exercise 3.37}}% +\subsection{\verified{Exercise 3.37}}% \label{sub:exercise-3.37} Assume that $\Pi$ is a partition of a set $A$. Define the relation $R_\Pi$ as follows: - $$xR_{\Pi}y \iff (\exists B \in \Pi)(x \in B \land y \in B).$$ + \begin{equation} + \label{sub:exercise-3.37-eq1} + xR_{\Pi}y \iff (\exists B \in \Pi)(x \in B \land y \in B). + \end{equation} Show that $R_\Pi$ is an equivalence relation on $A$. (This is a formalized version of the discussion at the beginning of this section.) \begin{proof} - TODO + \lean{Bookshelf/Enderton/Set/Relation} + {Enderton.Set.Chapter\_3.exercise\_3\_37} + + We prove that (i) $R_\Pi$ is reflexive on $B$, (ii) $R_\Pi$ is symmetric, and + (iii) $R_\Pi$ is transitive. + + \paragraph{(i)}% + + Let $x \in A$. + By definition of a \nameref{ref:partition}, there exists some nonempty set + $B \in \Pi$ such that $x \in B$. + Thus $(\exists B \in \Pi)(x \in B \land x \in B)$. + By \eqref{sub:exercise-3.37-eq1}, $\left< x, x \right> \in R_\Pi$. + Therefore $R_\Pi$ is reflexive on $A$. + + \paragraph{(ii)}% + + Let $\left< x, y \right> \in R_\Pi$. + By \eqref{sub:exercise-3.37-eq1}, there exists some $B \in \Pi$ such that + $x \in B \land y \in B$. + But then $y \in B \land x \in B$. + Thus $\left< y, x \right> \in R_\Pi$. + In other words, $R_\Pi$ is symmetric. + + \paragraph{(iii)}% + + Let $\left< x, y \right>, \left< y, z \right> \in R_\Pi$. + By \eqref{sub:exercise-3.37-eq1}, there exists some $B_1 \in \Pi$ such that + $x \in B_1 \land y \in B_1$. + Likewise there exists some $B_2 \in \Pi$ such that + $y \in B_2 \land z \in B_2$. + But $\Pi$ is a \nameref{ref:partition} meaning $y \in B_1$ and $y \in B_2$ + if $B_1 = B_2$. + Therefore $x \in B_1 \land z \in B_1$ and $\left< x, z \right> \in R_\Pi$. + In other words, $R_\Pi$ is transitive. \end{proof} \subsection{\sorry{Exercise 3.38}}% \label{sub:exercise-3.38} -Theorem 3P shows that $A / R$ is a partition of $A$ whenever $R$ is an - equivalence relation on $A$. +\nameref{sub:theorem-3p} shows that $A / R$ is a partition of $A$ whenever $R$ + is an equivalence relation on $A$. Show that if we start with the equivalence relation $R_\Pi$ of the preceding exercise, then the partition $A / R_\Pi$ is just $\Pi$. \begin{proof} + We prove that $\{[x]_{R_\Pi} \mid x \in A\} = \Pi$. + TODO \end{proof} diff --git a/Bookshelf/Enderton/Set/Chapter_3.lean b/Bookshelf/Enderton/Set/Chapter_3.lean index 9d7d183..67e86ce 100644 --- a/Bookshelf/Enderton/Set/Chapter_3.lean +++ b/Bookshelf/Enderton/Set/Chapter_3.lean @@ -1,6 +1,7 @@ import Bookshelf.Enderton.Set.Chapter_2 import Bookshelf.Enderton.Set.OrderedPair import Bookshelf.Enderton.Set.Relation +import Common.Logic.Basic import Mathlib.Tactic.CasesM /-! # Enderton.Set.Chapter_3 @@ -519,7 +520,19 @@ theorem theorem_3j_a {F : Set.HRelation α β} {A : Set α} {B : Set β} have ⟨x₁, hx₁⟩ := ran_exists hy refine ⟨x₁, ⟨mem_pair_imp_fst_mem_dom hx₁, hx₁⟩, ?_⟩ intro x₂ hx₂ - sorry + + have hG' : y ∈ dom G := by + rw [hG.right.left.right.left] + exact hF.right.right hy + have ⟨z, hz⟩ := dom_exists hG' + + have := hG.right.right + unfold comp at this + rw [Set.ext_iff] at this + have h₁ := (this (x₁, z)).mp ⟨y, hx₁, hz⟩ + have h₂ := (this (x₂, z)).mp ⟨y, hx₂.right, hz⟩ + simp only [Set.mem_setOf_eq] at h₁ h₂ + rw [h₁.right, h₂.right] · sorry /-- #### Theorem 3J (b) @@ -1326,8 +1339,6 @@ A ⊆ B → F⟦A⟧ ⊆ F⟦B⟧ theorem exercise_3_22_a {A B : Set α} {F : Set.HRelation α β} (h : A ⊆ B) : image F A ⊆ image F B := by show ∀ x, x ∈ image F A → x ∈ image F B - unfold image - simp only [Set.mem_setOf_eq] intro x hx have ⟨u, hu⟩ := hx have := h hu.left @@ -1347,7 +1358,6 @@ theorem exercise_3_22_b {A B : Set α} {F : Set.HRelation α β} _ = { v | ∃ u ∈ A, ∃ a, (u, a) ∈ G ∧ (a, v) ∈ F } := rfl _ = { v | ∃ a, ∃ u ∈ A, (u, a) ∈ G ∧ (a, v) ∈ F } := by ext p - simp only [Set.mem_setOf_eq] apply Iff.intro · intro ⟨u, hu, a, ha⟩ exact ⟨a, u, hu, ha⟩ @@ -1355,7 +1365,6 @@ theorem exercise_3_22_b {A B : Set α} {F : Set.HRelation α β} exact ⟨u, hu, a, ha⟩ _ = { v | ∃ a, (∃ u ∈ A, (u, a) ∈ G) ∧ (a, v) ∈ F } := by ext p - simp only [Set.mem_setOf_eq] apply Iff.intro · intro ⟨a, u, h⟩ exact ⟨a, ⟨u, h.left, h.right.left⟩, h.right.right⟩ @@ -1404,7 +1413,6 @@ theorem exercise_3_23_i {A : Set α} {B : Set.HRelation α β} {I : Set.Relation · show ∀ p, p ∈ restriction B A → p ∈ comp B I unfold restriction comp rw [hI] - simp only [Set.mem_setOf_eq, and_true] intro (x, y) hp refine ⟨x, ⟨hp.right, rfl⟩, hp.left⟩ @@ -1420,16 +1428,13 @@ theorem exercise_3_23_ii {A C : Set α} {I : Set.Relation α} _ = { v | ∃ u ∈ C, (u, v) ∈ I } := rfl _ = { v | ∃ u ∈ C, u ∈ A ∧ u = v } := by ext v - simp only [Set.mem_setOf_eq] apply Iff.intro · intro ⟨u, h₁, h₂⟩ rw [hI] at h₂ - simp only [Set.mem_setOf_eq] at h₂ exact ⟨u, h₁, h₂⟩ · intro ⟨u, h₁, h₂⟩ refine ⟨u, h₁, ?_⟩ · rw [hI] - simp only [Set.mem_setOf_eq] exact h₂ _ = { v | v ∈ C ∧ v ∈ A } := by ext v @@ -1455,7 +1460,6 @@ theorem exercise_3_24 {F : Set.HRelation α β} {A : Set β} _ = { x | ∃ y ∈ A, (x, y) ∈ F } := by simp only [mem_self_comm_mem_inv] _ = { x | x ∈ dom F ∧ (∃ y : β, (x, y) ∈ F ∧ y ∈ A) } := by ext x - simp only [Set.mem_setOf_eq] apply Iff.intro · intro ⟨y, hy, hyx⟩ exact ⟨mem_pair_imp_fst_mem_dom hyx, y, hyx, hy⟩ @@ -1488,7 +1492,6 @@ theorem exercise_3_25_b {G : Set.HRelation α β} (hG : isSingleValued G) intro h simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] at h have ⟨t, ⟨a, b, ⟨hab, hb, ha⟩⟩, ht⟩ := h - simp only [Set.mem_setOf_eq] rw [hb, ha] at hab exact ⟨mem_pair_imp_snd_mem_ran hab, single_valued_eq_unique hG hab ht⟩ · intro h @@ -1518,12 +1521,8 @@ theorem exercise_3_27 {F : Set.HRelation β γ} {G : Set.HRelation α β} apply And.intro · show ∀ x, x ∈ dom (comp F G) → x ∈ image (inv G) (dom F) intro x hx - have ⟨y, hy⟩ := dom_exists hx - unfold comp at hy - simp only [Set.mem_setOf_eq] at hy - have ⟨t, ht⟩ := hy + have ⟨y, t, ht⟩ := dom_exists hx have htF : t ∈ dom F := mem_pair_imp_fst_mem_dom ht.right - unfold image inv simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] exact ⟨t, htF, x, t, ht.left, rfl, rfl⟩ @@ -1636,9 +1635,7 @@ theorem exercise_3_28 {A : Set α} {B : Set β} have ⟨a, ha⟩ := hx rw [ha.right] show ∀ y, y ∈ image f a → y ∈ B - intro y hy - simp only [Set.mem_setOf_eq] at hy - have ⟨b, hb⟩ := hy + intro y ⟨b, hb⟩ have hz := mem_pair_imp_snd_mem_ran hb.right exact hf.right.right.right hz @@ -1675,18 +1672,355 @@ theorem exercise_3_29 {f : Set.HRelation α β} {G : Set.HRelation β (Set α)} have h₂ := single_valued_eq_unique hG.left.left hx₂.right hG₂ rw [← h₁, ← h₂] - rw [hG.right, ← hf.right.right] at hG₁ hG₂ - simp only [Set.mem_setOf_eq, and_true] at hG₁ hG₂ + rw [hG.right, ← hf.right.right] at hG₁ + simp only [Set.mem_setOf_eq, and_true] at hG₁ have ⟨t, ht⟩ := ran_exists hG₁ have : t ∈ {x ∈ A | (x, x₁) ∈ f} := by - simp only [Set.mem_setOf_eq] refine ⟨?_, ht⟩ rw [← hf.right.left] exact mem_pair_imp_fst_mem_dom ht rw [heq] at this - simp only [Set.mem_setOf_eq] at this exact single_valued_eq_unique hf.left this.right ht +/-- #### Theorem 3M + +If `R` is a symmetric and transitive relation, then `R` is an equivalence +relation on `fld R`. +-/ +theorem theorem_3m {R : Set.Relation α} + (hS : R.isSymmetric) (hT : R.isTransitive) + : R.isEquivalence (fld R) := by + refine ⟨?_, hS, hT⟩ + unfold isReflexive fld + intro x hx + apply Or.elim hx + · intro h + have ⟨y, hy⟩ := dom_exists h + have := hS hy + exact hT hy this + · intro h + have ⟨t, ht⟩ := ran_exists h + have := hS ht + exact hT this ht + +/-- #### Lemma 3N + +Assume that `R` is an equivalence relation on `A` and that `x` and `y` belong +to `A`. Then `[x]_R = [y]_R ↔ xRy`. +-/ +theorem lemma_3n {R : Set.Relation α} {A : Set α} {x y : α} + (hR : R.isEquivalence A) (_ : x ∈ A) (hy : y ∈ A) + : cell R x = cell R y ↔ (x, y) ∈ R := by + apply Iff.intro + · intro h + have : y ∈ cell R y := hR.left y hy + rwa [← h] at this + · intro h + rw [Set.ext_iff] + intro t + apply Iff.intro + · intro ht + have := hR.right.left h + exact hR.right.right this ht + · intro ht + exact hR.right.right h ht + +/-- #### Theorem 3P + +Assume that `R` is an equivalence relation on `A`. Then the set +`{[x]_R | x ∈ A}` of all equivalence classes is a partition of `P`. +-/ +theorem theorem_3p {R : Set.Relation α} {A : Set α} {P : Set (Set α)} + (hR : R.isEquivalence A) (hP : P = {cell R x | x ∈ A}) + : isPartition P A := by + refine ⟨?_, ?_, ?_⟩ + · -- Every member is nonempty. + intro p hp + rw [hP] at hp + have ⟨x, hx⟩ := hp + rw [← hx.right] + exact ⟨x, hR.left x hx.left⟩ + + · -- Every pair of members is disjoint. + intro xR hxR yR hyR h + by_contra nh + have nh' : Set.Nonempty (xR ∩ yR) := by + rw [← Set.nmem_singleton_empty] + exact nh + have ⟨z, hz⟩ := nh' + rw [hP] at hxR hyR + have ⟨x, hx⟩ := hxR + have ⟨y, hy⟩ := hyR + rw [← hx.right, ← hy.right] at hz + unfold cell at hz + simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hz + have hzy : (z, y) ∈ R := hR.right.left hz.right + have hxy : (x, y) ∈ R := hR.right.right hz.left hzy + have := (lemma_3n hR hx.left hy.left).mpr hxy + rw [hx.right, hy.right] at this + exact absurd this h + + · -- Every element of `A` is in `P`. + intro x hx + have := hR.left x hx + refine ⟨cell R x, ?_, this⟩ + · rw [hP] + exact ⟨x, hx, rfl⟩ + +/-- #### Exercise 3.32 (a) + +Show that `R` is symmetric **iff** `R⁻¹ ⊆ R`. +-/ +theorem exercise_3_32_a {R : Set.Relation α} + : isSymmetric R ↔ inv R ⊆ R := by + apply Iff.intro + · intro hR + show ∀ p, p ∈ inv R → p ∈ R + intro (x, y) hp + simp only [mem_self_comm_mem_inv] at hp + exact hR hp + · intro hR + unfold isSymmetric + intro x y hp + rw [← mem_self_comm_mem_inv] at hp + exact hR hp + +/-- #### Exercise 3.32 (b) + +Show that `R` is transitive **iff** `R ∘ R ⊆ R`. +-/ +theorem exercise_3_32_b {R : Set.Relation α} + : isTransitive R ↔ comp R R ⊆ R := by + apply Iff.intro + · intro hR + show ∀ p, p ∈ comp R R → p ∈ R + intro (x, y) hp + have ⟨t, ht⟩ := hp + exact hR ht.left ht.right + · intro hR + intro x y z hx hz + have : (x, z) ∈ comp R R := ⟨y, hx, hz⟩ + exact hR this + +/-- #### Exercise 3.33 + +Show that `R` is a symmetric and transitive relation **iff** `R = R⁻¹ ∘ R`. +-/ +theorem exercise_3_33 {R : Set.Relation α} + : isSymmetric R ∧ isTransitive R ↔ R = comp (inv R) R := by + have hR : comp (inv R) R = { p | ∃ t, (p.1, t) ∈ R ∧ (p.2, t) ∈ R } := by + ext p + unfold comp inv + simp only [Prod.exists, Set.mem_setOf_eq, Prod.mk.injEq] + apply Iff.intro + · intro ⟨t, ht, a, b, h⟩ + refine ⟨t, ht, ?_⟩ + rw [← h.right.right, ← h.right.left] + exact h.left + · intro ⟨t, ht⟩ + exact ⟨t, ht.left, p.snd, t, ht.right, rfl, rfl⟩ + + apply Iff.intro + · intro h + rw [Set.Subset.antisymm_iff] + apply And.intro + · show ∀ p, p ∈ R → p ∈ comp (inv R) R + intro (x, y) hp + have hy := h.left hp + have hx := h.right hp hy + rw [hR] + exact ⟨x, hx, hy⟩ + · show ∀ p, p ∈ comp (inv R) R → p ∈ R + intro (x, y) hp + rw [hR] at hp + have ⟨_, ht⟩ := hp + have := h.left ht.right + exact h.right ht.left this + · intro h + have hS : isSymmetric R := by + intro x y hp + have : inv R = R := by + calc inv R + _ = inv (comp (inv R) R) := by conv => lhs; rw [h] + _ = comp (inv R) (inv (inv R)) := by rw [comp_inv_eq_inv_comp_inv] + _ = comp (inv R) R := by rw [inv_inv_eq_self] + _ = R := h.symm + rwa [← this, mem_self_comm_mem_inv] + refine ⟨hS, ?_⟩ + intro x y z hx hy + have : (z, y) ∈ R := hS hy + rw [h, hR] + exact ⟨y, hx, this⟩ + +/-- #### Exercise 3.34 (a) + +Assume that `𝓐` is a nonempty set, every member of which is a transitive +relation. Is the set `⋂ 𝓐` a transitive relation? +-/ +theorem exercise_3_34_a {𝓐 : Set (Set.Relation α)} + (_ : Set.Nonempty 𝓐) (h𝓐 : ∀ A ∈ 𝓐, isTransitive A) + : isTransitive (⋂₀ 𝓐) := by + intro x y z hx hy + simp only [Set.mem_sInter] at * + intro A hA + have hx' := hx A hA + have hy' := hy A hA + exact h𝓐 A hA hx' hy' + +/-- #### Exercise 3.34 (b) + +Assume that `𝓐` is a nonempty set, every member of which is a transitive +relation. Is `⋃ 𝓐` a transitive relation? +-/ +theorem exercise_3_34_b {𝓐 : Set (Set.Relation ℕ)} + (_ : Set.Nonempty 𝓐) (h𝓐 : 𝓐 = {{(1, 2), (2, 3), (1, 3)}, {(2, 1)}}) + : (∀ A ∈ 𝓐, isTransitive A) ∧ ¬ isTransitive (⋃₀ 𝓐) := by + apply And.intro + · intro A hA + rw [h𝓐] at hA + simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at hA + apply Or.elim hA + · intro hA₁ + rw [hA₁] + intro x y z hx hy + simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Prod.mk.injEq] at * + casesm* _ ∨ _ + all_goals case _ hl hr => first + | {rw [hl.right] at hr; simp at hr} + | {rw [hl.left] at hr; simp at hr} + | {right; right; exact ⟨hl.left, hr.right⟩} + · intro hA₁ + rw [hA₁] + intro x y z hx hy + simp only [Set.mem_singleton_iff, Set.mem_insert_iff, Prod.mk.injEq] at * + rw [hx.right] at hy + simp at hy + · intro h + have h₁ : (1, 2) ∈ ⋃₀ 𝓐 := by + simp only [Set.mem_sUnion] + exact ⟨{(1, 2), (2, 3), (1, 3)}, by rw [h𝓐]; simp, by simp⟩ + have h₂ : (2, 1) ∈ ⋃₀ 𝓐 := by + simp only [Set.mem_sUnion] + exact ⟨{(2, 1)}, by rw [h𝓐]; simp, by simp⟩ + have h₃ : (1, 1) ∉ ⋃₀ 𝓐 := by + simp only [Set.mem_sUnion] + rw [h𝓐] + intro ⟨t, ht⟩ + simp only [Set.mem_singleton_iff, Set.mem_insert_iff] at ht + have := ht.right + apply Or.elim ht.left <;> + · intro ht₁ + rw [ht₁] at this + simp at this + exact absurd (h h₁ h₂) h₃ + +/-- #### Exercise 3.35 + +Show that for any `R` and `x`, we have `[x]_R = R⟦{x}⟧`. +-/ +theorem exercise_3_35 {R : Set.Relation α} {x : α} + : cell R x = image R {x} := by + calc cell R x + _ = { t | (x, t) ∈ R } := rfl + _ = { t | ∃ u ∈ ({x} : Set α), (u, t) ∈ R } := by simp + _ = image R {x} := rfl + +/-- #### Exercise 3.36 + +Assume that `f : A → B` and that `R` is an equivalence relation on `B`. Define +`Q` to be the set `{⟨x, y⟩ ∈ A × A | ⟨f(x), f(y)⟩ ∈ R}`. Show that `Q` is an +equivalence relation on `A`. +-/ +theorem exercise_3_36 {f : Set.HRelation α β} + {Q : Set.Relation α} {R : Set.Relation β} {A : Set α} {B : Set β} + (hf : mapsInto f A B) + (hR : isEquivalence R B) + (hQ : Q = { p | ∃ fx fy : β, (p.1, fx) ∈ f ∧ (p.2, fy) ∈ f ∧ (fx, fy) ∈ R }) + : isEquivalence Q A := by + refine ⟨?_, ?_, ?_⟩ + · unfold isReflexive + intro x hx + unfold mapsInto at hf + rw [← hf.right.left] at hx + have ⟨fx, hfx⟩ := dom_exists hx + have := hR.left fx (hf.right.right $ mem_pair_imp_snd_mem_ran hfx) + rw [hQ] + simp only [exists_and_left, Set.mem_setOf_eq] + exact ⟨fx, hfx, fx, hfx, this⟩ + · unfold isSymmetric + intro x y h + rw [hQ] at h + simp only [exists_and_left, Set.mem_setOf_eq] at h + have ⟨fx, hfx, fy, hfy, h'⟩ := h + have := hR.right.left h' + rw [hQ] + simp only [exists_and_left, Set.mem_setOf_eq] + exact ⟨fy, hfy, fx, hfx, this⟩ + · unfold isTransitive + intro x y z hx hy + rw [hQ] at hx hy + simp only [exists_and_left, Set.mem_setOf_eq] at hx hy + have ⟨fx, hfx, fy, hfy, h₁⟩ := hx + have ⟨fy₁, hfy₁, fz, hfz, h₂⟩ := hy + have hfy' : fy = fy₁ := single_valued_eq_unique hf.left hfy hfy₁ + rw [hfy'] at h₁ + rw [hQ] + simp only [exists_and_left, Set.mem_setOf_eq] + exact ⟨fx, hfx, fz, hfz, hR.right.right h₁ h₂⟩ + +/-- #### Exercise 3.37 + +Assume that `Π` is a partition of a set `A`. Define the relation `R` as follows: +``` +xRy ↔ (∃ B ∈ Π)(x ∈ B ∧ y ∈ B). +``` +Show that `R` is an equivalence relation on `A`. (This is a formalized version +of the discussion at the beginning of this section.) +-/ +theorem exercise_3_37 {P : Set (Set α)} {A : Set α} + (hP : isPartition P A) (R : Set.Relation α) + (hR : ∀ x y, (x, y) ∈ R ↔ ∃ B ∈ P, x ∈ B ∧ y ∈ B) + : isEquivalence R A := by + have hR' : R = { p | ∃ B ∈ P, p.1 ∈ B ∧ p.2 ∈ B } := by + ext p + have (x, y) := p + exact hR x y + refine ⟨?_, ?_, ?_⟩ + · unfold isReflexive + intro x hx + rw [hR'] + simp only [Set.mem_setOf_eq, and_self] + exact hP.right.right x hx + · unfold isSymmetric + intro x y h + rw [hR'] at h + simp only [Set.mem_setOf_eq] at h + have ⟨B, hB⟩ := h + rw [hR'] + simp only [Set.mem_setOf_eq] + conv at hB => right; rw [and_comm] + exact ⟨B, hB⟩ + · unfold isTransitive + intro x y z hx hy + rw [hR'] at hx hy + simp only [Set.mem_setOf_eq] at hx hy + have ⟨B₁, hB₁⟩ := hx + have ⟨B₂, hB₂⟩ := hy + unfold isPartition at hP + have hB : B₁ = B₂ := by + have hy₁ : y ∈ B₁ := hB₁.right.right + have hy₂ : y ∈ B₂ := hB₂.right.left + have hy := hP.right.left B₁ hB₁.left B₂ hB₂.left + rw [contraposition] at hy + simp at hy + suffices B₁ ∩ B₂ ≠ ∅ from hy this + intro h' + rw [Set.ext_iff] at h' + exact (h' y).mp ⟨hy₁, hy₂⟩ + rw [hR'] + simp only [Set.mem_setOf_eq] + exact ⟨B₁, hB₁.left, hB₁.right.left, by rw [hB]; exact hB₂.right.right⟩ +lemma test (h : ¬ p = q) : p ≠ q := by exact? end Relation end Enderton.Set.Chapter_3 \ No newline at end of file diff --git a/Bookshelf/Enderton/Set/Relation.lean b/Bookshelf/Enderton/Set/Relation.lean index a14e999..fc574c0 100644 --- a/Bookshelf/Enderton/Set/Relation.lean +++ b/Bookshelf/Enderton/Set/Relation.lean @@ -488,6 +488,52 @@ def toOrderedPairs (R : Relation α) : Set (Set (Set α)) := -- Notice here we are using `Set.image` and *not* `Set.Relation.image`. Set.image (fun (x, y) => OrderedPair x y) R +/-! ## Equivalence Classes -/ + +/-- +A binary `Relation` `R` is **reflexive** on `A` **iff** `xRx` for all `x ∈ A`. +-/ +def isReflexive (R : Relation α) (A : Set α) := ∀ a ∈ A, (a, a) ∈ R + +/-- +A binary `Relation` `R` is **symmetric** **iff** whenever `xRy` then `yRx`. +-/ +def isSymmetric (R : Relation α) := ∀ {x y : α}, (x, y) ∈ R → (y, x) ∈ R + +/-- +A binary `Relation` `R` is **transitive** **iff** whenever `xRy` and `yRz`, then +`xRz`. +-/ +def isTransitive (R : Relation α) := + ∀ {x y z : α}, (x, y) ∈ R → (y, z) ∈ R → (x, z) ∈ R + +/-- +`Relation` `R` is an **equivalence relation** on set `A` **iff** `R` is a binary +relation that is relexive on `A`, symmetric, and transitive. +-/ +def isEquivalence (R : Relation α) (A : Set α) := + isReflexive R A ∧ isSymmetric R ∧ isTransitive R + +/-- +A **partition** `Π` of a set `A` is a set of nonempty subsets of `A` that is +disjoint and exhaustive. +-/ +def isPartition (P : Set (Set α)) (A : Set α) := + (∀ p ∈ P, Set.Nonempty p) ∧ + (∀ a ∈ P, ∀ b, b ∈ P → a ≠ b → a ∩ b = ∅) ∧ + (∀ a ∈ A, ∃ p, p ∈ P ∧ a ∈ p) + +/-- +A cell of some partition induced by `Relation` `R`. +-/ +def cell (R : Relation α) (x : α) := { t | (x, t) ∈ R } + +/-- +The equivalence class of `x` modulo `R`. +-/ +def isEquivClass (R : Relation α) (A : Set α) (x : α) := + isEquivalence R A ∧ x ∈ fld R + end Relation end Set \ No newline at end of file diff --git a/Common/Logic/Basic.lean b/Common/Logic/Basic.lean index b8bed5a..a9bf1e5 100644 --- a/Common/Logic/Basic.lean +++ b/Common/Logic/Basic.lean @@ -17,6 +17,17 @@ Renaming of `not_or` to indicate its relationship to de Morgan's laws. -/ theorem not_or_de_morgan : ¬(p ∨ q) ↔ ¬p ∧ ¬q := not_or +/-- +The principle of contraposition. +-/ +theorem contraposition : (p → q) ↔ (¬q → ¬p) := by + apply Iff.intro + · intro h nq hp + exact absurd (h hp) nq + · intro h hp + by_contra nq + exact absurd hp (h nq) + /-- Universal quantification across nested set memberships can be commuted in either order.