Enderton. Additional equivalence relation exercises.
parent
c574b481af
commit
98ecc12995
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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.
|
||||
|
|
|
|||
Loading…
Reference in New Issue