Initial commit

4 files changed, 582 insertions, 0 deletions

diff --git a/library/relation/closure.tex b/library/relation/closure.tex
new file mode 100644
index 0000000..8eebf08
--- /dev/null
+++ b/library/relation/closure.tex
@@ -0,0 +1,28 @@
+\import{relation/properties.tex}
+\import{relation/equivalence.tex}
+
+\subsection{Closure operations on relations}
+
+\begin{definition}\label{reflexive_closure}
+    $\reflexiveClosure{X}{R} = R\union\identity{X}$.
+\end{definition}
+
+% reflexive closure of R is the smallest reflexive relation containing R
+\begin{proposition}\label{reflexive_closure_is_reflexive}
+    $\reflexiveClosure{X}{R}$ is reflexive on $X$.
+\end{proposition}
+
+\begin{definition}\label{reflexive_reduction}
+    $\reflexiveReduction{X}{R} = R\setminus\identity{X}$.
+\end{definition}
+
+\begin{definition}\label{symmetric_closure}
+    $\symmetricClosure{R} = R\union\converse{R}$.
+\end{definition}
+
+
+% LATER transitive closure
+
+% LATER reflexive transitive closure
+
+% LATER equivalence closure
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex
new file mode 100644
index 0000000..bda8486
--- /dev/null
+++ b/library/relation/equivalence.tex
@@ -0,0 +1,271 @@
+\import{set.tex}
+\import{set/partition.tex}
+\import{relation.tex}
+\import{order/quasiorder.tex}
+
+
+\subsection{Equivalences}
+
+% Sometimes also called "restricted equivalence".
+\begin{abbreviation}\label{partialequivalence}
+    $E$ is a partial equivalence iff
+    $E$ is transitive and symmetric.
+\end{abbreviation}
+
+\begin{proposition}\label{partialequivalence_is_quasireflexive}
+    Let $E$ be a partial equivalence.
+    Then $E$ is quasireflexive.
+\end{proposition}
+
+\begin{abbreviation}\label{equivalence}
+    $E$ is an equivalence iff
+    $E$ is a symmetric quasiorder.
+\end{abbreviation}
+
+\begin{abbreviation}\label{equivalence_on}
+    $E$ is an equivalence on $A$ iff
+    $E$ is a symmetric quasiorder on $A$.
+\end{abbreviation}
+
+\begin{proposition}\label{inters_of_family_of_equivalences_is_equivalence}
+    Let $F$ be a family of relations.
+    Suppose every element of $F$ is an equivalence.
+    Then $\inters{F}$ is an equivalence.
+\end{proposition}
+\begin{proof}
+    $\inters{F}$ is quasireflexive by \cref{quasireflexive,inters_destr,inters_iff_forall}.
+    $\inters{F}$ is symmetric by \cref{symmetric,inters_iff_forall,inters_destr}.
+    $\inters{F}$ is transitive by \cref{transitive,inters_iff_forall,inters_destr}.
+\end{proof}
+
+\begin{proposition}\label{inters_of_family_of_equivalences_on_a_set_is_equivalence_on_that_set}
+    Let $F$ be an inhabited family of relations.
+    Suppose every element of $F$ is an equivalence on $A$.
+    Then $\inters{F}$ is an equivalence on $A$.
+\end{proposition}
+\begin{proof}
+    $\inters{F}$ is reflexive on $A$ by \cref{inters_of_family_of_reflexive_relations_is_reflexive}.
+    $\inters{F}$ is symmetric.
+    $\inters{F}$ is transitive.
+\end{proof}
+% NOTE: the union of a family of equivalence relations is not necessarily an
+% equivalence relation because a binary union of transitive relations is not
+% necessarily transitive.
+
+
+\subsubsection{Equivalence classes}
+
+\begin{abbreviation}\label{equiv_class}
+    $\equivalenceClass{E}{a} = \downward{E}{a}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{equivclass_abbr}
+    The $E$-equivalence class of $a$ is $\equivalenceClass{E}{a}$.
+\end{abbreviation}
+
+\begin{proposition}\label{equivclasses_inhabited}
+    Let $E$ be an equivalence.
+    Let $a\in \fld{E}$.
+    Then $a\in\equivalenceClass{E}{a}$.
+\end{proposition}
+\begin{proof}
+    $a\mathrel{E} a$ by \cref{reflexive_on,quasireflexive_implies_reflexive_on_fld}.
+\end{proof}
+
+\begin{proposition}\label{equivclasses_inhabited_equivalenceon}
+    Let $E$ be an equivalence on $A$.
+    Let $a\in A$.
+    Then $a\in\equivalenceClass{E}{a}$.
+\end{proposition}
+\begin{proof}
+    $a\mathrel{E} a$ by \cref{reflexive_on}.
+\end{proof}
+
+\begin{proposition}\label{equiv_implies_equivanlence_classes_eq}
+    Let $E$ be an equivalence on $A$.
+    Let $a, b\in A$.
+    Suppose $a\mathrel{E} b$.
+    Then $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{equivclasses_eq_implies_equiv}
+    Let $E$ be an equivalence on $A$.
+    Let $a, b\in A$.
+    Suppose $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
+    Then $a\mathrel{E} b$.
+\end{proposition}
+
+\begin{proposition}\label{equiv_iff_equivclasses_eq}
+    Let $E$ be an equivalence on $A$.
+    Let $a, b\in A$.
+    Then $a\mathrel{E} b$ iff $\equivalenceClass{E}{a} = \equivalenceClass{E}{b}$.
+\end{proposition}
+
+\begin{proposition}\label{equivclasses_diseq_implies_disjoint}
+    Let $E$ be a partial equivalence.
+    Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$.
+    Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
+\end{proposition}
+\begin{proof}
+    Suppose not.
+    Take $c$ such that $c\in \equivalenceClass{E}{a},\equivalenceClass{E}{b}$.
+    Then $c\mathrel{E} a$ and
+         $c\mathrel{E} b$.
+    $E$ is symmetric.
+    Thus $a\mathrel{E} c$ by \hyperref[symmetric]{symmetry}.
+    $E$ is transitive.
+    Thus $a\mathrel{E} b$ by \hyperref[transitive]{transitivity}.
+    Then $b\mathrel{E} a$ by \hyperref[symmetric]{symmetry}.
+    %
+    Thus $a\in \equivalenceClass{E}{b}$ and $b\in \equivalenceClass{E}{a}$
+        by \cref{downward_closure_iff}.
+    Hence $\equivalenceClass{E}{a}\subseteq \equivalenceClass{E}{b}\subseteq \equivalenceClass{E}{a}$
+        by \cref{transitive_downward_subseteq}.
+    Contradiction by \cref{subseteq_antisymmetric}.
+\end{proof}
+
+\begin{corollary}\label{equivalence_equivclasses_diseq_implies_disjoint}
+    Let $E$ be an equivalence.
+    Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$.
+    Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
+\end{corollary}
+\begin{proof}
+    Follows by \cref{equivclasses_diseq_implies_disjoint}.
+\end{proof}
+
+\begin{corollary}\label{equivalenceon_equivclasses_diseq_implies_disjoint}
+    Let $E$ be an equivalence on $A$.
+    Suppose $\equivalenceClass{E}{a}\neq \equivalenceClass{E}{b}$.
+    Then $\equivalenceClass{E}{a}$ is disjoint from $\equivalenceClass{E}{b}$.
+\end{corollary}
+\begin{proof}
+    Follows by \cref{equivclasses_diseq_implies_disjoint}.
+\end{proof}
+
+
+\subsubsection{Quotients}
+
+\begin{definition}\label{quotient}
+    $\quotient{A}{E} = \{\equivalenceClass{E}{a}\mid a\in A\}$.
+\end{definition}
+
+%\begin{definition}\label{equivalenceclasses}
+%    $\equivalenceClasses{E} = \{\equivalenceClass{E}{a}\mid a\in\dom{E}\}$.
+%\end{definition}
+
+\begin{proposition}\label{quotient_emptyset}
+    $\quotient{\emptyset}{\emptyset} = \emptyset$.
+\end{proposition}
+
+
+\begin{proposition}\label{quotient_elems_disjoint}
+    Let $E$ be an equivalence on $A$.
+    Suppose $B,C\in\quotient{A}{E}$ and $B\neq C$.
+    Then $B$ is disjoint from $C$.
+\end{proposition}
+\begin{proof}
+    Take $b$ such that $B = \equivalenceClass{E}{b}$.
+    Take $c$ such that $C = \equivalenceClass{E}{c}$.
+    Then $B$ is disjoint from $C$ by \cref{equivalenceon_equivclasses_diseq_implies_disjoint}.
+\end{proof}
+
+\begin{proposition}\label{quotient_elems_inhabited}
+    Let $E$ be an equivalence on $A$.
+    Suppose $C\in\quotient{A}{E}$.
+    Then $C$ is inhabited.
+\end{proposition}
+\begin{proof}
+    Take $a\in A$ such that $C = \equivalenceClass{E}{a}$.
+    Then $a\in \equivalenceClass{E}{a}$.
+    $C$ is inhabited by \cref{quotient,inhabited,equivclasses_inhabited}.
+\end{proof}
+
+\begin{proposition}\label{quotient_elems_type}
+    Let $E$ be an equivalence on $A$.
+    Suppose $a\in C\in\quotient{A}{E}$.
+    Then $a\in A$.
+\end{proposition}
+\begin{proof}
+    Take $b\in A$ such that $C = \equivalenceClass{E}{b}$
+        by \cref{quotient}.
+    Then $a\mathrel{E} b$.
+    Thus $a\in A$ by \cref{times_tuple_elim,subseteq}.
+\end{proof}
+
+
+\begin{corollary}\label{quotient_notni_emptyset}
+    Let $E$ be an equivalence on $A$.
+    $\emptyset\notin\quotient{A}{E}$.
+\end{corollary}
+
+\begin{proposition}\label{quotient_partition}
+    Let $E$ be an equivalence on $A$.
+    $\quotient{A}{E}$ is a partition.
+\end{proposition}
+\begin{proof}
+    $\emptyset\notin\quotient{A}{E}$.
+    For all $B, C\in \quotient{A}{E}$ such that $B\neq C$ we have $B$ is disjoint from $C$.
+\end{proof}
+
+\begin{proposition}\label{quotient_partition_of}
+    Let $E$ be an equivalence on $A$.
+    $\quotient{A}{E}$ is a partition of $A$.
+\end{proposition}
+\begin{proof}
+    $\unions{(\quotient{A}{E})} = A$ 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}
diff --git a/library/relation/properties.tex b/library/relation/properties.tex
new file mode 100644
index 0000000..191b7c0
--- /dev/null
+++ b/library/relation/properties.tex
@@ -0,0 +1,202 @@
+\import{set.tex}
+\import{relation.tex}
+
+\subsection{Properties of relations}
+
+\begin{definition}\label{left_quasireflexive}
+    $R$ is left quasireflexive iff
+    for all $x, y$ such that $x\mathrel{R} y$
+    we have $x\mathrel{R}x$.
+\end{definition}
+
+\begin{definition}\label{right_quasireflexive}
+    $R$ is right quasireflexive iff
+    for all $x, y$ such that $x\mathrel{R} y$
+    we have $y\mathrel{R}y$.
+\end{definition}
+
+\begin{definition}\label{quasireflexive}
+    $R$ is quasireflexive iff
+    for all $x, y$ such that $x\mathrel{R} y$
+    we have $x\mathrel{R}x$ and $y\mathrel{R}y$.
+\end{definition}
+
+\begin{definition}\label{coreflexive}
+    $R$ is coreflexive iff
+    for all $x, y$ such that $x\mathrel{R} y$
+    we have $x = y$.
+\end{definition}
+
+\begin{definition}\label{reflexive_on}
+    $R$ is reflexive on $X$ iff
+    for all $x\in X$
+    we have $x\mathrel{R}x$.
+\end{definition}
+
+\begin{definition}\label{irreflexive}
+    $R$ is irreflexive iff
+    for all $x$ we have $(x,x)\notin R$.
+\end{definition}
+
+
+\begin{proposition}\label{quasireflexive_implies_reflexive_on_fld}
+    Suppose $R$ is quasireflexive.
+    Then $R$ is reflexive on $\fld{R}$.
+\end{proposition}
+
+\begin{proposition}\label{reflexive_on_fld_impliesquasireflexive}
+    Suppose $R$ is reflexive on $\fld{R}$.
+    Then $R$ is quasireflexive.
+\end{proposition}
+
+\begin{proposition}\label{inters_of_family_of_reflexive_relations_is_reflexive}
+    Let $F$ be an inhabited family of relations.
+    Suppose every element of $F$ is reflexive on $A$.
+    Then $\inters{F}$ is reflexive on $A$.
+\end{proposition}
+\begin{proof}
+    For all $a\in A$ we have for all $R\in F$ we have $a\mathrel{R} a$.
+    Thus for all $a\in A$ we have $a\mathrel{(\inters{F})} a$.
+\end{proof}
+
+\begin{definition}\label{antisymmetric}
+    $R$ is antisymmetric iff
+    for all $x, y$ such that $x\mathrel{R}y\mathrel{R}x$
+    we have $x = y$.
+\end{definition}
+
+\begin{definition}[Symmetry]\label{symmetric}
+    $R$ is symmetric iff
+    for all $x, y$ we have
+    $x\mathrel{R} y \iff y\mathrel{R}x$.
+\end{definition}
+
+\begin{definition}\label{asymmetric}
+    $R$ is asymmetric iff
+    for all $x, y$ such that
+    $x\mathrel{R} y$ we have $y\not\mathrel{R}x$.
+\end{definition}
+
+\begin{proposition}\label{asymmetric_implies_irreflexive}
+    Suppose $R$ is asymmetric.
+    Then $R$ is irreflexive.
+\end{proposition}
+
+\begin{proposition}\label{asymmetric_implies_antisymmetric}
+    Suppose $R$ is asymmetric.
+    Then $R$ is antisymmetric.
+\end{proposition}
+
+\begin{proposition}\label{antisymmetric_and_irreflexive_implies_asymmetric}
+    Suppose $R$ is antisymmetric.
+    Suppose $R$ is irreflexive.
+    Then $R$ is asymmetric.
+\end{proposition}
+
+% TODO
+%\begin{proposition}\label{symmetric_relation_eq_converse}
+%    Let $R$ be a symmetric relation.
+%    Then $\converse{R} = R$.
+%\end{proposition}
+%\begin{proof}
+%    Follows by set extensionality.
+%\end{proof}
+
+\begin{definition}[Transitivity]\label{transitive}
+    $R$ is transitive iff
+    for all $x, y, z$ such that $x\mathrel{R}y\mathrel{R}z$
+        we have $x\mathrel{R} z$.
+\end{definition}
+
+\begin{proposition}\label{transitive_downward_elem}
+    Suppose $R$ is transitive.
+    Suppose $a\in\downward{R}{b}$.
+    Suppose $c\in\downward{R}{a}$.
+    Then $c\in \downward{R}{b}$.
+\end{proposition}
+\begin{proof}
+    $c\mathrel{R} a\mathrel{R}b$.
+    Thus $c\mathrel{R} b$ by \hyperref[transitive]{transitivity}.
+\end{proof}
+
+\begin{proposition}\label{transitive_downward_subseteq}
+    Suppose $R$ is transitive.
+    Suppose $a\in\downward{R}{b}$.
+    Then $\downward{R}{a}\subseteq \downward{R}{b}$.
+\end{proposition}
+
+\begin{definition}\label{dense}
+    $R$ is dense iff
+    for all $x, z$ such that $x\mathrel{R}z$
+        there exists $y$ such that $x\mathrel{R}y\mathrel{R}z$.
+\end{definition}
+
+% Variation of connexity that does not depend on a carrier.
+\begin{definition}\label{quasiconnex}
+    $R$ is quasiconnex iff
+    for all $x, y\in\fld{R}$ such that $x\neq y$ we have
+        $x\mathrel{R}y$ or $y\mathrel{R}x$.
+\end{definition}
+
+% Also called "connected" (here reserved for topology),
+% "complete" (heavily overloaded), and total" (also overloaded).
+\begin{definition}\label{connex}
+    $R$ is connex on $X$ iff
+    for all $x, y\in X$ such that $x\neq y$ we have
+        $x\mathrel{R}y$ or $y\mathrel{R}x$.
+\end{definition}
+
+\begin{definition}\label{strongly_quasiconnex}
+    $R$ is strongly quasiconnex iff
+    for all $x, y\in\fld{R}$ we have
+        $x\mathrel{R}y$ or $y\mathrel{R}x$.
+\end{definition}
+
+\begin{definition}\label{strongly_connex}
+    $R$ is strongly connex on $X$ iff
+    for all $x, y\in X$ we have
+        $x\mathrel{R}y$ or $y\mathrel{R}x$.
+\end{definition}
+
+%\begin{proposition}\label{strongly_quasiconnex_implies_quasiconnex_and_quasireflexive}
+%    Suppose $R$ is strongly quasiconnex.
+%    Then $R$ is quasiconnex and quasireflexive.
+%\end{proposition}
+
+%\begin{proposition}\label{quasiconnex_and_quasireflexive_implies_strongly_quasiconnex}
+%    Suppose $R$ is quasiconnex and quasireflexive.
+%    Then $R$ is strongly quasiconnex.
+%\end{proposition}
+
+\begin{proposition}\label{strongly_quasiconnex_iff_quasiconnex_and_quasireflexive}
+    $R$ is strongly quasiconnex iff
+    $R$ is quasiconnex and quasireflexive.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{quasiconnex,strongly_quasiconnex,quasireflexive_implies_reflexive_on_fld,reflexive_on,fld,reflexive_on_fld_impliesquasireflexive}.
+\end{proof}
+
+\begin{proposition}\label{connex_reaches_all_or_all_but_one}
+    Suppose $R$ is connex on $A$.
+    Let $a, b\in A\setminus\ran{R}$.
+    Then $a = b$.
+\end{proposition}
+\begin{proof}
+    Suppose not.
+    $a, b\in A$.
+    Then $(a, b)\in R$ or $(b,a)\in R$ by \cref{connex}.
+    $(a, b)\notin R$.
+    $(b, a)\notin R$.
+    Thus $a = b$.
+\end{proof}
+
+
+\begin{definition}\label{righteuclidean}
+    $R$ is right Euclidean iff
+    for all $a,b,c$ such that $a\mathrel{R}b,c$ we have $b\mathrel{R}c$.
+\end{definition}
+
+\begin{definition}\label{lefteuclidean}
+    $R$ is left Euclidean iff
+    for all $a,b,c$ such that $a,b\mathrel{R}c$ we have $a\mathrel{R}b$.
+\end{definition}
diff --git a/library/relation/uniqueness.tex b/library/relation/uniqueness.tex
new file mode 100644
index 0000000..68b01de
--- /dev/null
+++ b/library/relation/uniqueness.tex
@@ -0,0 +1,81 @@
+\import{set.tex}
+\import{relation.tex}
+
+
+\subsection{Injective relations}
+
+% Injective relations are also called "left-unique"
+\begin{definition}\label{injective}
+    $R$ is injective iff for all $a,a',b$ such that $a, a'\mathrel{R} b$ we have $a = a'$.
+\end{definition}
+
+\begin{abbreviation}\label{leftunique}
+    $R$ is left-unique iff $R$ is injective.
+\end{abbreviation}
+
+\begin{proposition}\label{subseteq_of_injective_is_injective}
+    Suppose $S\subseteq R$.
+    Suppose $R$ is injective.
+    Then $S$ is injective.
+\end{proposition}
+
+\begin{proposition}\label{restrl_injective}
+    Suppose $R$ is injective.
+    Then $\restrl{R}{A}$ is injective.
+\end{proposition}
+\begin{proof}
+    $\restrl{R}{A}\subseteq R$.
+\end{proof}
+
+\begin{proposition}\label{circ_injective}
+    Suppose $R$ and $S$ are injective.
+    Then $S\circ R$ is injective.
+\end{proposition}
+
+\begin{proposition}\label{identity_injective}
+    Then $\identity{A}$ is injective.
+\end{proposition}
+
+\subsection{Right-unique relations}
+
+% also called "functional" or "univalent"
+\begin{definition}\label{rightunique}
+    $R$ is right-unique iff
+    for all $a,b,b'$ such that $a\mathrel{R} b, b'$ we have $b = b'$.
+\end{definition}
+
+\begin{abbreviation}\label{onetoone}
+    $R$ is one-to-one iff $R$ is right-unique and injective.
+\end{abbreviation}
+
+\begin{proposition}\label{subseteq_of_rightunique_is_rightunique}
+    Suppose $S\subseteq R$.
+    Suppose $R$ is right-unique.
+    Then $S$ is right-unique.
+\end{proposition}
+
+\begin{proposition}\label{circ_rightunique}
+    Suppose $R$ and $S$ are right-unique.
+    Then $S\circ R$ is right-unique.
+\end{proposition}
+
+
+
+\subsection{Left-total relations}
+
+\begin{definition}\label{lefttotal}
+    $R$ is left-total on $A$ iff
+    for all $a\in A$ there exists $b$ such that $a\mathrel{R} b$.
+\end{definition}
+
+
+\subsection{Right-total relations}
+
+\begin{definition}\label{righttotal}
+    $R$ is right-total on $B$ iff
+    for all $b\in B$ there exists $a$ such that $a\mathrel{R} b$.
+\end{definition}
+
+\begin{abbreviation}\label{surjective}
+    $R$ is surjective on $B$ iff $R$ is right-total on $B$.
+\end{abbreviation}