diff options
| -rw-r--r-- | library/relation/equivalence.tex | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex index bda8486..0c5dbfa 100644 --- a/library/relation/equivalence.tex +++ b/library/relation/equivalence.tex @@ -221,51 +221,57 @@ \begin{definition}\label{equivalence_from_partition} - $\equivfrompartition{P} = \{(a, b)\mid a\in A, b\in A\mid \exists C\in P.\ a, b\in C\}$. + $\equivfrompartition{P}{A} = \{(a, b)\mid a\in A, b\in A\mid \exists C\in P.\ a, b\in C\}$. \end{definition} \begin{proposition}\label{equivalence_from_partition_intro} Let $P$ be a partition of $A$. Let $a,b\in A$. Suppose $a,b\in C\in P$. - Then $a\mathrel{\equivfrompartition{P}} b$. + Then $a\mathrel{\equivfrompartition{P}{A}} b$. \end{proposition} \begin{proposition}\label{equivalence_from_partition_reflexive} Let $P$ be a partition of $A$. - $\equivfrompartition{P}$ is reflexive on $A$. + $\equivfrompartition{P}{A}$ is reflexive on $A$. \end{proposition} \begin{proposition}\label{equivalence_from_partition_symmetric} Let $P$ be a partition. - $\equivfrompartition{P}$ is symmetric. + $\equivfrompartition{P}{A}$ is symmetric. \end{proposition} \begin{proof} - Follows by \cref{symmetric,equivalence_from_partition,notin_emptyset}. + Omitted. \end{proof} \begin{proposition}\label{equivalence_from_partition_transitive} Let $P$ be a partition. - $\equivfrompartition{P}$ is transitive. + $\equivfrompartition{P}{A}$ is transitive. \end{proposition} +\begin{proof} + Omitted. +\end{proof} \begin{proposition}\label{equivalence_from_partition_is_equivalence} Let $P$ be a partition of $A$. - $\equivfrompartition{P}$ is an equivalence on $A$. + $\equivfrompartition{P}{A}$ is an equivalence on $A$. \end{proposition} +\begin{proof} + Omitted. +\end{proof} \begin{proposition}\label{equivalence_from_quotient} Let $E$ be an equivalence on $A$. - Then $\equivfrompartition{\quotient{A}{E}} = E$. + Then $\equivfrompartition{\quotient{A}{E}}{A} = E$. \end{proposition} \begin{proof} - Follows by set extensionality. + Omitted. \end{proof} \begin{proposition}\label{partition_eq_quotient_by_equivalence_from_partition} Let $P$ be a partition of $A$. - Then $\quotient{A}{\equivfrompartition{P}} = P$. + Then $\quotient{A}{\equivfrompartition{P}{A}} = P$. \end{proposition} \begin{proof} - Follows by set extensionality. + Omitted. \end{proof} |