diff options
| -rw-r--r-- | library/relation/equivalence.tex | 107 | ||||
| -rw-r--r-- | source/Syntax/Lexicon.hs | 1 |
2 files changed, 57 insertions, 51 deletions
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex index 87f70af..0c5dbfa 100644 --- a/library/relation/equivalence.tex +++ b/library/relation/equivalence.tex @@ -219,54 +219,59 @@ \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 + +\begin{definition}\label{equivalence_from_partition} + $\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}{A}} b$. +\end{proposition} + +\begin{proposition}\label{equivalence_from_partition_reflexive} + Let $P$ be a partition of $A$. + $\equivfrompartition{P}{A}$ is reflexive on $A$. +\end{proposition} + +\begin{proposition}\label{equivalence_from_partition_symmetric} + Let $P$ be a partition. + $\equivfrompartition{P}{A}$ is symmetric. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{equivalence_from_partition_transitive} + Let $P$ be a partition. + $\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}{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}}{A} = E$. +\end{proposition} +\begin{proof} + 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}{A}} = P$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index b5e4f58..463dd18 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -109,6 +109,7 @@ prefixOps = , ([Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "fst")) , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd")) , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow")) + , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg")) , (ConsSymbol, (NonAssoc, "cons")) , (PairSymbol, (NonAssoc, "pair")) -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply")) |