definition of equivalence_from_partition can proof false in everything.tex

2 files changed, 57 insertions, 51 deletions

diff --git a/library/everything.tex b/library/everything.tex
index 61bccb2..783679f 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -16,12 +16,13 @@
 \import{relation/uniqueness.tex}
 \import{function.tex}
 \import{ordinal.tex}
-%\import{nat.tex}
+\import{nat.tex}
 \import{cardinal.tex}
 \import{algebra/magma.tex}
 \import{algebra/semigroup.tex}
 \import{algebra/monoid.tex}
 \import{algebra/group.tex}
+
 \import{order/order.tex}
 %\import{order/semilattice.tex}
 \import{topology/topological-space.tex}
@@ -33,3 +34,7 @@
 \begin{proposition}\label{trivial}
     $x = x$.
 \end{proposition}
+
+%\begin{proposition}\label{safe}
+%    Contradiction.
+%\end{proposition}
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex
index bda8486..87f70af 100644
--- a/library/relation/equivalence.tex
+++ b/library/relation/equivalence.tex
@@ -219,53 +219,54 @@
 \end{proof}
 
 
-
-\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\}$.
-\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$.
-\end{proposition}
-
-\begin{proposition}\label{equivalence_from_partition_reflexive}
-    Let $P$ be a partition of $A$.
-    $\equivfrompartition{P}$ is reflexive on $A$.
-\end{proposition}
-
-\begin{proposition}\label{equivalence_from_partition_symmetric}
-    Let $P$ be a partition.
-    $\equivfrompartition{P}$ is symmetric.
-\end{proposition}
-\begin{proof}
-    Follows by \cref{symmetric,equivalence_from_partition,notin_emptyset}.
-\end{proof}
-
-\begin{proposition}\label{equivalence_from_partition_transitive}
-    Let $P$ be a partition.
-    $\equivfrompartition{P}$ is transitive.
-\end{proposition}
-
-\begin{proposition}\label{equivalence_from_partition_is_equivalence}
-    Let $P$ be a partition of $A$.
-    $\equivfrompartition{P}$ is an equivalence on $A$.
-\end{proposition}
-
-\begin{proposition}\label{equivalence_from_quotient}
-    Let $E$ be an equivalence on $A$.
-    Then $\equivfrompartition{\quotient{A}{E}} = E$.
-\end{proposition}
-\begin{proof}
-    Follows by set extensionality.
-\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$.
-\end{proposition}
-\begin{proof}
-    Follows by set extensionality.
-\end{proof}
+%
+%\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\}$.
+%\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$.
+%\end{proposition}
+%
+%\begin{proposition}\label{equivalence_from_partition_reflexive}
+%    Let $P$ be a partition of $A$.
+%    $\equivfrompartition{P}$ is reflexive on $A$.
+%\end{proposition}
+%
+%\begin{proposition}\label{equivalence_from_partition_symmetric}
+%    Let $P$ be a partition.
+%    $\equivfrompartition{P}$ is symmetric.
+%\end{proposition}
+%\begin{proof}
+%    Follows by \cref{symmetric,equivalence_from_partition,notin_emptyset}.
+%\end{proof}
+%
+%\begin{proposition}\label{equivalence_from_partition_transitive}
+%    Let $P$ be a partition.
+%    $\equivfrompartition{P}$ is transitive.
+%\end{proposition}
+%
+%\begin{proposition}\label{equivalence_from_partition_is_equivalence}
+%    Let $P$ be a partition of $A$.
+%    $\equivfrompartition{P}$ is an equivalence on $A$.
+%\end{proposition}
+%
+%\begin{proposition}\label{equivalence_from_quotient}
+%    Let $E$ be an equivalence on $A$.
+%    Then $\equivfrompartition{\quotient{A}{E}} = E$.
+%\end{proposition}
+%\begin{proof}
+%    Follows by set extensionality.
+%\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$.
+%\end{proposition}
+%\begin{proof}
+%    Follows by set extensionality.
+%\end{proof}
+%
\ No newline at end of file