Initial commit

1 files changed, 202 insertions, 0 deletions

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}