Merge branch 'main' into main

1 files changed, 33 insertions, 0 deletions

diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex
new file mode 100644
index 0000000..2dd026d
--- /dev/null
+++ b/library/topology/order-topology.tex
@@ -0,0 +1,33 @@
+\import{topology/topological-space.tex}
+\import{order/order.tex}
+
+\section{Order Topology}
+
+\begin{abbreviation}\label{open_interval}
+    $z \in \oointervalof{x}{y}$ iff $x \mathrel{R} y$ and $x \mathrel{R} z$ and $z \mathrel{R} y$.
+    %$\oointervalof{x}{y}{X} = \{ z \mid x \in X, y \in X, z \in X x \mathrel{R} y \wedge x \mathrel{R} z \wedge z \mathrel{R} y\}$. 
+\end{abbreviation}
+
+\begin{struct}\label{order_topology}
+    A ordertopology space $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $<$
+    \end{enumerate}
+    such that 
+    \begin{enumerate}
+        \item \label{order_topology_1} $<$ is a strict order on $X$
+        \item \label{order_topology_2}  
+        \item \label{order_topology_3}
+        \item \label{order_topology_4}
+        \item \label{order_topology}
+        \item \label{order_topology}
+        \item \label{order_topology}
+    \end{enumerate}
+\end{struct}
+
+
+
+%\begin{definition}\label{order_topology}
+%    $X$ has the order topology iff for all $x,y \in X$ $X$ has a strict order $R$ and $\oointervalof{x}{y}{X} \in \opens[X]$ and $X$ is a topological space.
+%    %$O$ is the order Topology on $X$ iff for all $x,y \in X$ $X$ has a strict order $R$ and $(x,y) \in O$ and $O$ is . 
+%\end{definition}