From 0c82b10cd3ac1787838038b4b443f79cbb1612d9 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 26 Jun 2024 13:56:47 +0200
Subject: Working at the numbers.tex

---
 .gitignore             |  1 +
 library/everything.tex |  8 ++++----
 library/numbers.tex    | 26 ++++++++++++++++++++++++++
 3 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index cd7aa0f..656e54b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -41,6 +41,7 @@ premseldump/
 haddocks/
 stack.yaml.lock
 zf*.svg
+check/
 
 
 
diff --git a/library/everything.tex b/library/everything.tex
index 783679f..29b97b7 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -29,12 +29,12 @@
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
-\import{numbers.tex}
+%\import{numbers.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
 \end{proposition}
 
-%\begin{proposition}\label{safe}
-%    Contradiction.
-%\end{proposition}
+\begin{proposition}\label{safe}
+    Contradiction.
+\end{proposition}
diff --git a/library/numbers.tex b/library/numbers.tex
index 1837ae8..f13214d 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -1,5 +1,6 @@
 \import{order/order.tex}
 \import{relation.tex}
+\import{set/suc.tex}
 
 \section{The real numbers}
 
@@ -15,6 +16,11 @@
     $x \rmul y$ is a set.
 \end{signature}
 
+%Structure TODO:
+% Take as may axioms as needed  - Tarski Axioms of reals
+%Implement Naturals -> Integer -> rationals -> reals 
+
+
 \subsection{Basic axioms of the reals}
 
 \begin{axiom}\label{reals_axiom_zero_in_reals}
@@ -29,6 +35,26 @@
     $\zero \neq 1$.
 \end{axiom}
 
+\begin{inductive}\label{naturals_subset_reals}
+    Define $\naturals \subseteq \reals$ inductively as follows.
+    \begin{enumerate}
+        \item $\zero \in \naturals$.
+        \item If $n\in \naturals$, then $\successor{n} \in \naturals$. 
+    \end{enumerate}
+\end{inductive}
+
+%\begin{axiom}\label{negativ_is_set}
+%    $\negativ{x}$ is a set.
+%\end{axiom}
+
+%\begin{axiom}\label{negativ_of}
+%    $\negativ{x} \in \reals$ iff $x\in \reals$.
+%\end{axiom}
+%
+%\begin{axiom}\label{negativ_behavior}
+%    $x + \negativ{x} = \zero$.
+%\end{axiom}
+
 \begin{definition}\label{reals_definition_order_def}
     $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$.
 \end{definition}
-- 
cgit v1.2.3