Merge branch 'main' into main

9 files changed, 597 insertions, 3 deletions

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 48934bd..a79bd2f 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1 +1,82 @@
-\section{Groups}
+\import{algebra/monoid.tex}
+\section{Group}
+
+\begin{struct}\label{group}
+    A group $G$ is a monoid such that
+    \begin{enumerate}
+        \item\label{group_inverse} for all $g \in \carrier[G]$ there exist $h \in \carrier[G]$ such that $\mul[G](g, h) =\neutral[G]$.
+    \end{enumerate} 
+\end{struct}   
+
+\begin{corollary}\label{group_implies_monoid}
+    Let $G$ be a group. Then $G$ is a monoid.
+\end{corollary}
+
+\begin{abbreviation}\label{cfourdot}
+    $g \cdot h = \mul(g,h)$.
+\end{abbreviation}
+
+\begin{lemma}\label{neutral_is_idempotent}
+    Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$.
+\end{lemma}
+
+\begin{lemma}\label{group_divison_right}
+    Let $G$ be a group. Let $a,b,c \in G$.
+    Then $a \cdot c = b \cdot c$ iff $a = b$.
+\end{lemma}
+\begin{proof}
+    Take $a,b,c \in G$ such that $a \cdot c = b \cdot c$.
+    There exist $c' \in G$ such that $c \cdot c' = \neutral[G]$.
+    Therefore $a \cdot c = b \cdot c$ iff $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$.
+    \begin{align*}
+        (a \cdot c) \cdot c'
+            &= a \cdot (c \cdot c')
+                \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\
+            &= a \cdot \neutral[G]
+                \explanation{by \cref{group_inverse}}\\
+            &= a
+                \explanation{by \cref{group_implies_monoid,monoid_right}}
+    \end{align*}
+    \begin{align*}
+        (b \cdot c) \cdot c'
+            &= b \cdot (c \cdot c')
+                \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\
+            &= b \cdot \neutral[G]
+                \explanation{by \cref{group_inverse}}\\
+            &= b
+                \explanation{by \cref{group_implies_monoid,monoid_right}}
+    \end{align*}
+    $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$ iff $a \cdot c = b \cdot c$ by assumption. 
+    $a = b$ iff $a \cdot c = b \cdot c$ by assumption.
+\end{proof}
+
+
+\begin{proposition}\label{leftinverse_eq_rightinverse}
+    Let $G$ be a group and assume $a \in G$.
+    Then there exist $b\in G$ 
+    such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$.
+\end{proposition}
+\begin{proof}
+    There exist $b \in G$ such that $a \cdot b = \neutral[G]$.
+    There exist $c \in G$ such that $b \cdot c = \neutral[G]$.
+    $a \cdot b = \neutral[G]$.
+    $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$.
+    $(a \cdot b) \cdot c = a \cdot (b \cdot c)$.
+    $a \cdot \neutral[G] = \neutral[G] \cdot c$.
+    $c = c \cdot \neutral[G]$.
+    $c = \neutral[G] \cdot c$.
+    $a \cdot \neutral[G] = c \cdot \neutral[G]$.
+    $a \cdot \neutral[G] = c$ by \cref{monoid_right,group_divison_right}.
+    $a = c$ by \cref{monoid_right,group_divison_right,neutral_is_idempotent}.
+    $b \cdot a = b \cdot c$.
+    $b \cdot a = \neutral[G]$.
+\end{proof}
+
+\begin{definition}\label{group_abelian}
+    $G$ is an abelian group iff $G$ is a group and for all $g,h \in G$ $\mul[G](g,h) = \mul[G](h,g)$. 
+\end{definition}
+
+
+\begin{definition}\label{group_automorphism}
+    Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. 
+\end{definition}
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
new file mode 100644
index 0000000..06fcb50
--- /dev/null
+++ b/library/algebra/monoid.tex
@@ -0,0 +1,19 @@
+\import{algebra/semigroup.tex}
+\section{Monoid}
+
+\begin{struct}\label{monoid}
+    A monoid $A$ is a semigroup equipped with
+    \begin{enumerate}
+        \item $\neutral$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{monoid_type} $\neutral[A]\in \carrier[A]$.
+        \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$.
+        \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$.
+    \end{enumerate}
+\end{struct}
+
+\begin{corollary}\label{monoid_implies_semigroup}
+    Let $A$ be a monoid. Then $A$ is a semigroup.
+\end{corollary}
\ No newline at end of file
diff --git a/library/everything.tex b/library/everything.tex
index 9b85f83..61bccb2 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -20,12 +20,15 @@
 \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}
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
+\import{numbers.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/nat.tex b/library/nat.tex
index 529ba54..ac9a141 100644
--- a/library/nat.tex
+++ b/library/nat.tex
@@ -1,5 +1,5 @@
 \import{set/suc.tex}
-
+\import{set.tex}
 
 \section{Natural numbers}
 
@@ -17,5 +17,46 @@
 \end{axiom}
 
 \begin{abbreviation}\label{naturalnumber}
-    $n$ is a natural number iff $n\in\naturals$.
+    $n$ is a natural number iff $n\in \naturals$.
+\end{abbreviation}
+
+\begin{lemma}\label{emptyset_in_naturals}
+    $\emptyset\in\naturals$.    
+\end{lemma}
+
+\begin{signature}\label{addition_is_set}
+    $x+y$ is a set.
+\end{signature}
+
+\begin{axiom}\label{addition_on_naturals}
+    $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number.
+\end{axiom}
+
+\begin{abbreviation}\label{zero_is_emptyset}
+    $\zero = \emptyset$.
 \end{abbreviation}
+
+\begin{axiom}\label{addition_axiom_1}
+    For all $x \in \naturals$ $x + \zero = \zero + x = x$.
+\end{axiom}
+
+\begin{axiom}\label{addition_axiom_2}
+    For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$.
+\end{axiom}
+
+\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+    $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
+\end{lemma}
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/library/numbers.tex b/library/numbers.tex
new file mode 100644
index 0000000..5dd06da
--- /dev/null
+++ b/library/numbers.tex
@@ -0,0 +1,195 @@
+\import{nat.tex}
+\import{order/order.tex}
+\import{relation.tex}
+
+\section{The real numbers}
+
+%TODO: Implementing Notion for negativ number such as -x.
+
+%TODO:
+%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher
+%\cdot für multiklikation verwenden. 
+%< für die relation benutzen.
+% sup und inf einfügen
+
+\begin{signature}
+    $\reals$ is a set.
+\end{signature}
+
+\begin{signature}
+    $x + y$ is a set.
+\end{signature}
+
+\begin{signature}
+    $x \times y$ is a set.
+\end{signature}
+
+\begin{axiom}\label{one_in_reals}
+    $1 \in \reals$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_order}
+    $\lt[\reals]$ is an order on $\reals$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_strictorder}
+    $\lt[\reals]$ is a strict order.
+\end{axiom}
+
+\begin{abbreviation}\label{less_on_reals}
+    $x < y$ iff $(x,y) \in \lt[\reals]$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greater_on_reals}
+    $x > y$ iff $y < x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{lesseq_on_reals}
+    $x \leq y$ iff it is wrong that $x > y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greatereq_on_reals}
+    $x \geq y$ iff it is wrong that $x < y$.
+\end{abbreviation}
+
+\begin{axiom}\label{reals_axiom_dense}
+    For all $x,y \in \reals$ if $x < y$ then 
+    there exist $z \in \reals$ such that $x < z$ and $z < y$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_order_def}
+    $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x + z = y$.
+\end{axiom}
+
+\begin{lemma}\label{reals_one_bigger_than_zero}
+    $\zero < 1$.
+\end{lemma}
+
+
+\begin{axiom}\label{reals_axiom_assoc}
+    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \times y) \times z = x \times (y \times z)$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_kommu}
+    For all $x,y \in \reals$ $x + y = y + x$ and $x \times y = y \times x$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_zero_in_reals}
+    $\zero \in \reals$.
+\end{axiom}
+  
+\begin{axiom}\label{reals_axiom_zero}
+    For all $x \in \reals$ $x + \zero = x$. 
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_one}
+    For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_add_invers}
+    For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$.
+\end{axiom}
+
+
+\begin{axiom}\label{reals_axiom_mul_invers}
+    For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \times y = 1$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_disstro1}
+    For all $x,y,z \in \reals$ $x \times (y + z) = (x \times y) + (x \times z)$.
+\end{axiom}
+
+\begin{proposition}\label{reals_disstro2}
+    For all $x,y,z \in \reals$ $(y + z) \times x = (y \times x) + (z \times x)$.
+\end{proposition}
+
+\begin{proposition}\label{reals_reducion_on_addition}
+    For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
+\end{proposition}
+
+\begin{axiom}\label{reals_axiom_dedekind_complete}
+    For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$
+    such that $x < z < y$.
+\end{axiom}
+
+
+\begin{lemma}\label{order_reals_lemma1}
+    For all $x,y,z \in \reals$ such that $\zero < x$ 
+    if $y < z$ 
+    then $(y \times x) < (z \times x)$.
+\end{lemma}
+
+\begin{lemma}\label{order_reals_lemma2}
+    For all $x,y,z \in \reals$ such that $\zero < x$ 
+    if $y < z$ 
+    then $(x \times y) < (x \times z)$.
+\end{lemma}
+
+
+\begin{lemma}\label{order_reals_lemma3}
+    For all $x,y,z \in \reals$ such that $x < \zero$ 
+    if $y < z$ 
+    then $(x \times z) < (x \times y)$.
+\end{lemma}
+
+\begin{lemma}\label{o4rder_reals_lemma}
+    For all $x,y \in \reals$ if $x > y$ then $x \geq y$.
+\end{lemma}
+
+\begin{lemma}\label{order_reals_lemma5}
+    For all $x,y \in \reals$ if $x < y$ then $x \leq y$.
+\end{lemma}
+
+\begin{lemma}\label{order_reals_lemma6}
+    For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$.
+\end{lemma}
+
+\begin{axiom}\label{reals_axiom_minus}
+    For all $x \in \reals$ $x - x = \zero$.
+\end{axiom}
+
+\begin{lemma}\label{reals_minus}
+    Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$.
+\end{lemma}
+
+%\begin{definition}\label{reasl_supremum} %expaction "there exists" after \mid
+%    $\rsup{X} = \{z \mid \text{ $z \in \reals$ and for all $x,y$ such that $x \in X$ and $y,x \in \reals$ and $x < y$ we have $z \leq y$ }\}$.
+%\end{definition}
+
+\begin{definition}\label{upper_bound}
+    $x$ is an upper bound of $X$ iff for all $y \in X$ we have $x > y$.
+\end{definition}
+
+\begin{definition}\label{least_upper_bound}
+    $x$ is a least upper bound of $X$ iff $x$ is an upper bound of $X$ and for all $y$ such that $y$ is an upper bound of $X$ we have $x \leq y$.
+\end{definition}
+
+\begin{lemma}\label{supremum_unique}
+    %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$.
+    If $x$ is a least upper bound of $X$ and $y$ is a least upper bound of $X$ then $x = y$.
+\end{lemma}
+
+\begin{definition}\label{supremum_reals}
+    $x$ is the supremum of $X$ iff $x$ is a least upper bound of $X$.
+\end{definition}
+
+
+
+
+\begin{definition}\label{lower_bound}
+    $x$ is an lower bound of $X$ iff for all $y \in X$ we have $x < y$.
+\end{definition}
+
+\begin{definition}\label{greatest_lower_bound}
+    $x$ is a greatest lower bound of $X$ iff $x$ is an lower bound of $X$ and for all $y$ such that $y$ is an lower bound of $X$ we have $x \geq y$.
+\end{definition}
+
+\begin{lemma}\label{infimum_unique}
+    %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$.
+    If $x$ is a greatest lower bound of $X$ and $y$ is a greatest lower bound of $X$ then $x = y$.
+\end{lemma}
+
+\begin{definition}\label{infimum_reals}
+    $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
+\end{definition}
+
diff --git a/library/order/order.tex b/library/order/order.tex
index 339bad8..1b7692f 100644
--- a/library/order/order.tex
+++ b/library/order/order.tex
@@ -1,6 +1,7 @@
 \import{relation.tex}
 \import{relation/properties.tex}
 \import{order/quasiorder.tex}
+\section{Order}
 
 % also called "(partial) ordering" or "partial order" to contrast with connex (i.e. "total") orders.
 \begin{abbreviation}\label{order}
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index d8cfeaf..15910f9 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -1,4 +1,6 @@
 \import{topology/topological-space.tex}
+\import{set.tex}
+\import{set/powerset.tex}
 
 \subsection{Topological basis}
 
@@ -48,3 +50,70 @@
     $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$
     \\ such that $x\in V\subseteq U$}\right\}$.
 \end{definition}
+
+\begin{lemma}\label{emptyset_in_genopens}
+    Assume $B$ is a topological basis for $X$.
+    $\emptyset \in \genOpens{B}{X}$.
+\end{lemma}
+
+\begin{lemma}\label{all_is_in_genopens}
+    Assume $B$ is a topological basis for $X$.
+    $X \in \genOpens{B}{X}$.
+\end{lemma}
+\begin{proof}
+    $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+    $\unions{B} \in \genOpens{B}{X}$.
+    $X \subseteq \unions{B}$.
+\end{proof}
+
+\begin{lemma}\label{union_in_genopens}
+    Assume $B$ is a topological basis for $X$.
+    For all $F\subseteq \genOpens{B}{X}$ we have $\unions{F}\in\genOpens{B}{X}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
+\begin{lemma}\label{inters_in_genopens}
+    Assume $B$ is a topological basis for $X$.
+    %For all $A, C$ 
+    If $A\in \genOpens{B}{X}$ and $C\in \genOpens{B}{X}$ then $(A\inter C) \in \genOpens{B}{X}$.
+\end{lemma}
+\begin{proof}
+    
+    Show $(A \inter C) \in \pow{X}$.
+    \begin{subproof}
+        $(A \inter C) \subseteq X$ by assumption.
+    \end{subproof}
+    Therefore for all $A, C \in \genOpens{B}{X}$ we have $(A \inter C) \in \pow{X}$.
+    
+
+    Show for all $x\in (A\inter C)$ there exists $W \in B$
+    such that $x\in W$ and $W \subseteq (A\inter C)$.
+    \begin{subproof}
+        Fix $x \in (A\inter C)$.
+        There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by assumption.  %TODO: Warum muss hier by assumtion hin?
+        There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by assumption.
+        There exist $W \in B$ such that $x \in W$ and $W \subseteq v'$ and $W \subseteq V''$ by assumption.
+        
+        Show $W \subseteq (A\inter C)$.
+        \begin{subproof}
+            %$W \subseteq v'$ and $W \subseteq V''$.
+            For all $y \in W$ we have $y \in V'$ and $y \in V''$ by assumption.
+        \end{subproof}
+    \end{subproof}
+    %Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
+    %such that $x\in W$ and $W \subseteq (A\inter C)$.
+
+    $(A\inter C) \in \genOpens{B}{X}$ by assumption.
+    
+ 
+\end{proof}
+
+
+
+
+
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
new file mode 100644
index 0000000..1c6a0ca
--- /dev/null
+++ b/library/topology/metric-space.tex
@@ -0,0 +1,152 @@
+\import{topology/topological-space.tex}
+\import{numbers.tex}
+\import{function.tex}
+\import{set/powerset.tex}
+\import{topology/basis.tex}
+
+\section{Metric Spaces}
+
+\begin{definition}\label{metric}
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
+    for all $x,y,z \in M$ we have 
+        $f(x,x) = \zero$ and 
+        $f(x,y) = f(y,x)$ and
+        $f(x,y) \leq f(x,z) + f(z,y)$ and
+        if $x \neq y$ then $\zero < f(x,y)$.
+\end{definition}
+
+\begin{definition}\label{open_ball}
+    $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric on $M$ and $f(x,z) < r$ } \}$.
+\end{definition}
+
+
+
+%\begin{definition}\label{induced_topology}
+%    $O$ is the induced topology of $d$ in $M$ iff 
+%    $O \subseteq \pow{M}$ and
+%    $d$ is a metric on $M$ and 
+%    for all $x,r,A,B,C$ 
+%        such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$
+%        we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$.
+%\end{definition}
+
+%\begin{definition}
+%    $\projcetfirst{A} = \{a \mid \exists x \in X \text{there exist $x \i }  \}$
+%\end{definition}
+
+\begin{definition}\label{set_of_balls}
+    $\balls{d}{M} = \{ O \in \pow{M} \mid \text{there exists $x,r$ such that $r \in \reals$ and $x \in M$ and $O = \openball{r}{x}{d}$ } \}$.
+\end{definition}
+
+
+%\begin{definition}\label{toindsas}
+%    $\metricopens{d}{M} = \{O \in \pow{M} \mid \text{
+%        $d$ is a metric on $M$ and
+%        for all $x,r,A,B,C$ 
+%        such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$
+%        we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$.
+%    }  \}$.
+%    
+%\end{definition}
+
+\begin{definition}\label{metricopens}
+    $\metricopens{d}{M} = \genOpens{\balls{d}{M}}{M}$.
+\end{definition}
+
+
+\begin{theorem}
+    Let $d$ be a metric on $M$.
+    $M$ is a topological space.
+\end{theorem}
+
+
+
+
+%TODO: \metric_opens{d} =  {hier die construction für topology} DONE.
+%TODO: Die induzierte topology definieren und dann in struct verwenden.
+
+
+\begin{struct}\label{metric_space}  
+    A metric space $M$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\metric$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item \label{metric_space_metric}                   $\metric[M]$ is a metric on $M$.
+        \item \label{metric_space_topology}                 $M$ is a topological space.
+        \item \label{metric_space_opens}                    $\metricopens{ \metric[M] }{M} = \opens[M]$.
+    \end{enumerate}
+\end{struct}
+
+\begin{abbreviation}\label{descriptive_syntax_for_openball1}
+    $U$ is an open ball in $M$ of $x$ with radius $r$ iff $x \in M$ and $M$ is a metric space and $U = \openball{r}{x}{\metric[M]}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{descriptive_syntax_for_openball2}
+    $U$ is an open ball in $M$ iff there exist $x \in M$ such that there exist $r \in \reals$ such that $U$ is an open ball in $M$ of $x$ with radius $r$.
+\end{abbreviation}
+
+\begin{lemma}\label{union_of_open_balls_is_open}
+    Let $M$ be a metric space.
+    For all $U,V \subseteq M$ if $U$, $V$ are open balls in $M$ then $U \union V$ is open in $M$.
+\end{lemma}
+
+
+%\begin{definition}\label{lenght_of_interval} %TODO: take minus if its implemented
+%    $\lenghtinterval{x}{y} = r$ 
+%\end{definition}
+
+
+
+
+
+
+\begin{lemma}\label{metric_implies_topology}
+    Let $M$ be a set, and let $f$ be a metric on $M$.
+    Then $M$ is a metric space.
+\end{lemma}
+
+
+
+
+
+%\begin{struct}\label{metric_space}  
+%    A metric space $M$ is a onesorted structure equipped with
+%    \begin{enumerate}
+%        \item $\metric$
+%    \end{enumerate}
+%    such that
+%    \begin{enumerate}
+%        \item \label{metric_space_d}                        $\metric[M]$ is a function from $M \times M$ to $\reals$.
+%        \item \label{metric_space_distence_of_a_point}      $\metric[M](x,x) = \zero$.
+%        \item \label{metric_space_positiv}                  for all $x,y \in M$ if $x \neq y$ then $\zero < \metric[M](x,y)$.
+%        \item \label{metric_space_symetrie}                 $\metric[M](x,y) = \metric[M](y,x)$.
+%        \item \label{metric_space_triangle_equation}        for all $x,y,z \in M$ $\metric[M](x,y) < \metric[M](x,z) + \metric[M](z,y)$ or $\metric[M](x,y) = \metric[M](x,z) + \metric[M](z,y)$.
+%        \item \label{metric_space_topology}                 $M$ is a topological space.
+%        \item \label{metric_space_opens}                    for all $x \in M$ for all $r \in \reals$ $\{z \in M \mid \metric[M](x,z) < r\} \in \opens$.
+%    \end{enumerate}
+%\end{struct}
+
+%\begin{definition}\label{open_ball}
+%    $\openball{r}{x}{M} = \{z \in M \mid \metric(x,z) < r\}$.
+%\end{definition}
+
+%\begin{proposition}\label{open_ball_is_open}
+%    Let $M$ be a metric space,let $r \in \reals $, let $x$ be an element of $M$.
+%    Then $\openball{r}{x}{M} \in \opens[M]$.
+%\end{proposition}
+
+
+
+
+
+
+%TODO:  - Basis indudiert topology lemma
+%       - Offe Bälle sind basis
+
+% Was danach kommen soll bleibt offen, vll buch oder in proof wiki
+% Trennungsaxiom, 
+
+% Notaionen aufräumen damit das gut gemercht werden kann.
+
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}