From 868857d2764a26668e32d3e4f9764f728fb162a4 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 25 Jun 2024 16:52:32 +0200
Subject: Update equivalence.tex

---
 library/relation/equivalence.tex | 28 +++++++++++++++++-----------
 1 file changed, 17 insertions(+), 11 deletions(-)

(limited to 'library/relation/equivalence.tex')

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}
-- 
cgit v1.2.3