From 9abb88060e5bb6405e603dcbe499794e3e181040 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 31 Mar 2024 18:57:17 +0200
Subject: Possible_Bug

In File test.tex line 51 could not be proven, error massage is in the new file error.txt
---
 library/everything.tex | 1 +
 1 file changed, 1 insertion(+)

(limited to 'library/everything.tex')

diff --git a/library/everything.tex b/library/everything.tex
index 9b85f83..599bc27 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -26,6 +26,7 @@
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
+\import{test.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
-- 
cgit v1.2.3


From 15deff4df111d86c84d808f1c9cc4e30013287d0 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Thu, 11 Apr 2024 13:37:03 +0200
Subject: Formalisation of groups and monoids

The test.tex file was deleted and all formalisations of groups and monoids was moved to the fitting document of the library. Some proof steps of the new formalisation were optimized for proof time
---
 Error.txt                  | 16 ---------
 latex/stdlib.tex           |  3 +-
 library/algebra/group.tex  | 83 +++++++++++++++++++++++++++++++++++++++++++++-
 library/algebra/monoid.tex | 19 +++++++++++
 library/everything.tex     |  3 +-
 library/test.tex           | 54 ------------------------------
 6 files changed, 105 insertions(+), 73 deletions(-)
 delete mode 100644 Error.txt
 create mode 100644 library/algebra/monoid.tex
 delete mode 100644 library/test.tex

(limited to 'library/everything.tex')

diff --git a/Error.txt b/Error.txt
deleted file mode 100644
index 7aa836a..0000000
--- a/Error.txt
+++ /dev/null
@@ -1,16 +0,0 @@
-stack exec zf -- library/test.tex 
-Verification failed: prover found countermodel
-fof(leftinverse_eq_rightinverse,conjecture,fa=fc).
-fof(monoid_right,axiom,![XA]:(monoid(XA)=>![Xa]:(elem(Xa,s__carrier(XA))=>apply(s__mul(XA),pair(Xa,s__neutral(XA)))=Xa))).
-fof(leftinverse_eq_rightinverse1,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=fc).
-fof(leftinverse_eq_rightinverse2,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(fc,s__neutral(fG)))).
-fof(leftinverse_eq_rightinverse3,axiom,fc=apply(s__mul(fG),pair(s__neutral(fG),fc))).
-fof(leftinverse_eq_rightinverse4,axiom,fc=apply(s__mul(fG),pair(fc,s__neutral(fG)))).
-fof(leftinverse_eq_rightinverse5,axiom,apply(s__mul(fG),pair(fa,s__neutral(fG)))=apply(s__mul(fG),pair(s__neutral(fG),fc))).
-fof(leftinverse_eq_rightinverse6,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(fa,apply(s__mul(fG),pair(fb,fc))))).
-fof(leftinverse_eq_rightinverse7,axiom,apply(s__mul(fG),pair(apply(s__mul(fG),pair(fa,fb)),fc))=apply(s__mul(fG),pair(s__neutral(fG),fc))).
-fof(leftinverse_eq_rightinverse8,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)).
-fof(leftinverse_eq_rightinverse9,axiom,apply(s__mul(fG),pair(fb,fc))=s__neutral(fG)&elem(fc,s__carrier(fG))).
-fof(leftinverse_eq_rightinverse10,axiom,apply(s__mul(fG),pair(fa,fb))=s__neutral(fG)&elem(fb,s__carrier(fG))).
-fof(leftinverse_eq_rightinverse11,axiom,elem(fa,s__carrier(fG))).
-fof(leftinverse_eq_rightinverse12,axiom,group(fG)).
\ No newline at end of file
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index 4921363..e545395 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -36,6 +36,8 @@
     \input{../library/cardinal.tex}
     \input{../library/algebra/magma.tex}
     \input{../library/algebra/semigroup.tex}
+    \input{../library/algebra/monoid.tex}
+    \input{../library/algebra/group.tex}
     %\input{../library/algebra/quasigroup.tex}
     %\input{../library/algebra/loop.tex}
     \input{../library/order/order.tex}
@@ -43,5 +45,4 @@
     \input{../library/topology/topological-space.tex}
     \input{../library/topology/basis.tex}
     \input{../library/topology/disconnection.tex}
-    \input{../library/test.tex}
 \end{document}
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 599bc27..a5166af 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -20,13 +20,14 @@
 \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{test.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/test.tex b/library/test.tex
deleted file mode 100644
index d30bbba..0000000
--- a/library/test.tex
+++ /dev/null
@@ -1,54 +0,0 @@
-\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} %muss hier ein enumerate hin
-        \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}
-
-
-\section{Group}
-
-\begin{struct}\label{group}
-    A group $A$ is a monoid such that
-    \begin{enumerate}
-        \item\label{group_inverse} for all $a \in \carrier[A]$ there exist $b \in \carrier[A]$ such that $\mul[A](a, b) =\neutral[A]$.
-    \end{enumerate} 
-\end{struct}    
-
-\begin{abbreviation}\label{cfourdot}
-    $a\cdot b = \mul(a,b)$.
-\end{abbreviation}
-
-\begin{lemma}\label{neutral_is_idempotent}
-    Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$.
-\end{lemma}
-
-\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}.
-    $a = c$ by \cref{monoid_right}.
-    $b \cdot a = b \cdot c$.
-    $b \cdot a = \neutral[G]$.
-\end{proof}
\ No newline at end of file
-- 
cgit v1.2.3


From cfd5061ced34f061e84ecca2a266f8f4cd01ce36 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 30 Apr 2024 12:26:13 +0200
Subject: Adding the first formalisation of reals

---
 latex/naproche.sty                  |   5 +-
 latex/stdlib.tex                    |   1 +
 library/everything.tex              |   1 +
 library/nat.tex                     |  41 ++++++-----
 library/numbers.tex                 | 140 ++++++++++++++++++++++++++++++++++++
 library/topology/order-topology.tex |   7 ++
 6 files changed, 175 insertions(+), 20 deletions(-)
 create mode 100644 library/numbers.tex
 create mode 100644 library/topology/order-topology.tex

(limited to 'library/everything.tex')

diff --git a/latex/naproche.sty b/latex/naproche.sty
index d975f21..cb65fe7 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -127,8 +127,9 @@
 \newcommand{\Univ}[1]{\fun{Univ}(#1)}
 \newcommand{\upward}[2]{#2^{\uparrow #1}}
 \newcommand{\LeftOrb}[2]{#2\cdot #1}
-\newcommand{\addpair}{\mathcal{H}}
-%\newcommand{\add}[2]{(#1 + #2)}
+\newcommand{\integers}{\mathcal{Z}}
+\newcommand{\zero}{0}
+\newcommand{\one}{1}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index e545395..dba42a2 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -45,4 +45,5 @@
     \input{../library/topology/topological-space.tex}
     \input{../library/topology/basis.tex}
     \input{../library/topology/disconnection.tex}
+    \input{../library/numbers.tex}
 \end{document}
diff --git a/library/everything.tex b/library/everything.tex
index a5166af..61bccb2 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -28,6 +28,7 @@
 \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 849c610..ac9a141 100644
--- a/library/nat.tex
+++ b/library/nat.tex
@@ -24,34 +24,39 @@
     $\emptyset\in\naturals$.    
 \end{lemma}
 
-%\begin{abbreviation}\label{zero_is_emptyset}
-%    $0 = \emptyset$.
-%\end{abbreviation}
+\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}
 
-%\begin{definition}\label{additionpair}
-%    $x$ is an Additionpair iff $x \in ((\naturals\times \naturals)\times \naturals)$. 
-%\end{definition}
 
-%\begin{lemma}\label{zero_is_in_naturals}
-%    Let $n\in \naturals$. $((n, \emptyset), n)$ is an Additionpair.
-%\end{lemma}
 
-%\begin{definition}\label{valid_additionpair}
-%    $x$ is a vaildaddition iff there exist $n \in \naturals$ we have $x = ((0, n), n)$.
-%\end{definition}
 
 
 
-\begin{axiom}\label{addpair_set}
-    $\addpair$ is a set.
-\end{axiom}
 
 
 
 
-\begin{axiom}\label{addition_naturals}
-    $x \in \addpair$ iff $x \in ((\naturals\times \naturals)\times \naturals)$ and there exist $n \in \naturals$ such that $x = ((n, \emptyset), n)$.
-\end{axiom} 
 
 
 
diff --git a/library/numbers.tex b/library/numbers.tex
new file mode 100644
index 0000000..93623fa
--- /dev/null
+++ b/library/numbers.tex
@@ -0,0 +1,140 @@
+\import{nat.tex}
+\import{order/order.tex}
+\import{relation.tex}
+
+\section{The real numbers}
+
+\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$.
+    %$\reals$ is an ordered set.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_strictorder}
+    $\lt[\reals]$ is a strict order.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_dense}
+    For all $x,y \in \reals$ if $(x,y)\in \lt[\reals]$ then 
+    there exist $z \in \reals$ such that $(x,z) \in \lt[\reals]$ and $(z,y) \in \lt[\reals]$.
+    
+    %For all $X,Y \subseteq \reals$ if for all $x,y$ $x\in X$ and $y \in Y$ such that $x \lt[\reals] y$ 
+    %then there exist a $z \in \reals$ such that if $x \neq z$ and $y \neq z$ $x \lt[\reals] z$ and $z \lt[\reals] y$.
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_order_def}
+    $(x,y) \in \lt[\reals]$ iff there exist $z \in \reals$ such that $(\zero, z) \in \lt[\reals]$ and $x + z = y$.
+\end{axiom}
+
+\begin{lemma}\label{reals_one_bigger_than_zero}
+    $(\zero,1) \in \lt[\reals]$.
+\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_one_in_reals}
+%    $\one \in \reals$.
+%\end{axiom}
+    
+\begin{axiom}\label{reals_axiom_zero}
+    %There exist $\zero \in \reals$ such that 
+    For all $x \in \reals$ $x + \zero = x$. 
+\end{axiom}
+
+\begin{axiom}\label{reals_axiom_one}
+    %There exist $1 \in \reals$ such that 
+    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}
+
+%TODO: Implementing Notion for negativ number such as -x.
+
+%\begin{abbreviation}\label{reals_notion_minus}
+%    $y = -x$ iff $x + y = \zero$.
+%\end{abbreviation}                         %This abbrevation result in a killed process.
+
+\begin{axiom}\label{reals_axiom_mul_invers}
+    For all $x \in \reals$ there exist $y \in \reals$ such that  $x \neq \zero$ and $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{signature}
+    $\invers$ is a set.
+\begin{signature}
+
+%TODO:
+%x \rless y in einer signatur hinzufügen und  dann axiom x+z = y und dann \rlt in def per iff
+%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher
+%\cdot für multiklikation verwenden. 
+%< für die relation benutzen.
+
+%\begin{signature}
+%    $y^{\rightarrow}$ is a function.
+%\end{signature}
+
+%\begin{axiom}\label{notion_multi_invers}
+%    If $y \in \reals$ then $\invers{y} \in \reals$ and $y \times y^{\rightarrow} = 1$.
+%\end{axiom}
+
+%\begin{abbreviation}\label{notion_fraction}
+%    $\frac{x}{y} = x \times y^{\rightarrow}$.
+%\end{abbreviation}
+
+\begin{lemma}\label{order_reals_lemma1}
+    For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ 
+    if $(y,z) \in \lt[\reals]$ 
+    then $((y \times x), (z \times x)) \in \lt[\reals]$.
+\end{lemma}
+
+\begin{lemma}\label{order_reals_lemma2}
+    For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ 
+    if $(y,z) \in \lt[\reals]$ 
+    then $((x \times y), (x \times z)) \in \lt[\reals]$.
+\end{lemma}
+
+
+\begin{lemma}\label{order_reals_lemma3}
+    For all $x,y,z \in \reals$ such that $(x,\zero) \in \lt[\reals]$ 
+    if $(y,z) \in \lt[\reals]$ 
+    then $((x \times z), (x \times y)) \in \lt[\reals]$.
+\end{lemma}
diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex
new file mode 100644
index 0000000..afa8755
--- /dev/null
+++ b/library/topology/order-topology.tex
@@ -0,0 +1,7 @@
+\import{topology/topological-space.tex}
+
+\section{Order Topology}
+
+\begin{definition}
+    A 
+\end{definition}
-- 
cgit v1.2.3