From 6eea98cf3e66a07251e6370ea948898799d5055b Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 13 Apr 2024 13:01:14 +0200
Subject: first formalisation of addition on naturals

We try to Implement the Addition on natural numbers by a relation on N \times N to N such that some of the axioms of the addition holds
---
 library/nat.tex | 40 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 38 insertions(+), 2 deletions(-)

(limited to 'library/nat.tex')

diff --git a/library/nat.tex b/library/nat.tex
index 529ba54..849c610 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,41 @@
 \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{abbreviation}\label{zero_is_emptyset}
+%    $0 = \emptyset$.
+%\end{abbreviation}
+
+%\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} 
+
+
+
-- 
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/nat.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

