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

---
 library/everything.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'library/everything.tex')

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}
-- 
cgit v1.2.3


From cbac8ca4a5bf8ff38af3e512956ea1e468965194 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sun, 21 Jul 2024 12:26:20 +0200
Subject: Further Formalisation on numbers

---
 latex/naproche.sty     |   1 +
 library/everything.tex |   2 +-
 library/numbers.tex    | 165 ++++++++++++++++++++++++++++++++-----------------
 3 files changed, 110 insertions(+), 58 deletions(-)

(limited to 'library/everything.tex')

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 476d3dd..7ef2359 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -132,6 +132,7 @@
 \newcommand{\integers}{\mathcal{Z}}
 \newcommand{\zero}{0}
 \newcommand{\one}{1}
+\newcommand{\rmul}{\cdot}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
diff --git a/library/everything.tex b/library/everything.tex
index 29b97b7..b966197 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -29,7 +29,7 @@
 \import{topology/basis.tex}
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
-%\import{numbers.tex}
+\import{numbers.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/numbers.tex b/library/numbers.tex
index 4ccba67..0bfae2d 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -18,34 +18,6 @@
     $x \rmul y$ is a set.
 \end{signature}
 
-\begin{axiom}\label{reals_axiom_order}
-    $\lt[\reals]$ is an order on $\reals$.
-\end{axiom}
-
-\begin{abbreviation}\label{lesseq_on_reals}
-    $x \leq y$ iff $(x,y) \in \lt[\reals]$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{less_on_reals}
-    $x < y$ iff it is wrong that $y \leq x$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{greater_on_reals}
-    $x > y$ iff $y \leq x$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{greatereq_on_reals}
-    $x \geq y$ iff it is wrong that $x < y$.
-\end{abbreviation}
-
-\begin{abbreviation}\label{is_positiv}
-    $x$ is positiv iff $x > \zero$.
-\end{abbreviation}
-
-
-%Structure TODO:
-% Take as may axioms as needed  - Tarski Axioms of reals
-%Implement Naturals -> Integer -> rationals -> reals 
 
 
 \subsection{Creation of natural numbers}
@@ -384,14 +356,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $n,m \in \reals$ we have $(n + m) \in \reals$.
 \end{axiom}
 
-\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_assoc}
-    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
-\end{axiom}
 
 \begin{axiom}\label{reals_axiom_kommu}
     For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$.
@@ -417,31 +382,72 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$.
 \end{axiom}
 
-\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{axiom}\label{reals_disstro2}
     For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
 \end{axiom}
 
-
 \begin{axiom}\label{reals_reducion_on_addition}
     For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
 \end{axiom}
 
-\begin{axiom}\label{zero_less_one}
-    $\zero < 1$.
+\begin{abbreviation}\label{rless}
+    $x < y$ iff $x \rless y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{less_on_reals}
+    $x \leq y$ iff it is wrong that $y < x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greater_on_reals}
+    $x > y$ iff $y \leq x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greatereq_on_reals}
+    $x \geq y$ iff it is wrong that $x < y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{is_positiv}
+    $x$ is positiv iff $x > \zero$.
+\end{abbreviation}
+
+
+
+
+
+\begin{axiom}\label{tarski1}
+    For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$.
+\end{axiom}
+
+\begin{axiom}\label{tarski2}
+    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{tarski3}
+    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{axiom}\label{reals_axiom_order_def}
-    Suppose $x,y,z,w \in \reals$.
-    If $x + y < z + w$ then $x < z \lor y < w$.
+\begin{axiom}\label{tarski4}
+    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
+\end{axiom}
+
+\begin{axiom}\label{tarski5}
+    For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$.
 \end{axiom}
 
 
+\begin{axiom}\label{tarski8}
+    $\zero < 1$.
+\end{axiom}
+
+\begin{axiom}\label{labelordersossss}
+    For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$.
+\end{axiom}
 
+\begin{axiom}\label{nocheinschoeneslabel}
+    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. 
+\end{axiom}
 
 
 \subsection{The Intergers}
@@ -465,8 +471,8 @@ Such that we can introduce the integers and raitionals as smooth as possible.
 \end{lemma}
 \begin{proof}
     \begin{byCase}
-        \caseOf{$m = \zero$.} Trivial.%Follows by \cref{neg_of_zero,minus,neg,reals_add}.
-        \caseOf{$m \neq \zero$.} Trivial.% Follows by \cref{neg_of_zero,minus,neg,reals_add}.
+        \caseOf{$m = \zero$.} Trivial.
+        \caseOf{$m \neq \zero$.} Trivial.
     \end{byCase}
 \end{proof}
 
@@ -496,16 +502,31 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
 \end{lemma}
 \begin{proof}
-    Let $P = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
-    \begin{byCase}
-        \caseOf{$\integers \subseteq P$.} Trivial.
-        \caseOf{$P \subseteq \integers$.} Trivial.
-    \end{byCase}
+    Omitted.
 \end{proof}
 
+\begin{abbreviation}\label{positiv_real_number}
+    $r$ is a positiv real number iff $r > \zero$ and $r \in \reals$.
+\end{abbreviation}
 
 
 
+\begin{proposition}\label{integers_negativ_times_negativ_is_positiv}
+    Suppose $n,m \in \integers$.
+    Suppose $n < \zero$ and $m < \zero$.
+    Then $n \rmul m > \zero$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+    %$n \neq \zero$ and $m \neq \zero$.
+    %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$.
+    %There exists $n' \in \reals$ such that $n' + n = \zero$.
+    %There exists $m' \in \reals$ such that $m' + m = \zero$.
+\end{proof}
+
+%TODO: negativ * negativ = positiv.
+
+
 \subsection{The Rationals}
 
 \begin{axiom}\label{invers_reals}
@@ -520,26 +541,56 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     $\naturalsPlus = \naturals \setminus \{\zero\}$.
 \end{abbreviation}
 
-\begin{definition}\label{rationals}
+\begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen
     $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$.
 \end{definition}
 
+\begin{abbreviation}\label{nominator}
+    $z$ is nominator of $q$ iff there exists $n \in \naturalsPlus$ such that $q = \rfrac{z}{n}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{denominator}
+    $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$.
+\end{abbreviation}
+
+%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal}
+%    Suppose $p,q \in \rationals$.
+%    Suppose $z \in \naturals$.
+%    Suppose $p$ is positiv.
+%    Suppose $q$ is positiv.
+%    Suppose $z$ is nominator of $p$.
+%    Suppose $z$ is nominator of $p$.
+%    Suppose $p'$ is denominator of $p$.
+%    Suppose $q'$ is denominator of $q$.
+%    Then $p \leq q$ iff $p' \geq q'$.
+%\end{proposition}
+
+
+%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one}
+%    For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$.
+%\end{theorem}
+
+% TODO:  Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, 
 
 
 \subsection{Order on the reals}
 
+
+
 \begin{lemma}\label{plus_one_order}
     For all $r\in \reals$ we have $ r < r + 1$.
 \end{lemma}
 \begin{proof}
-    %Follows by \cref{reals_axiom_one,reals_axiom_order,reals_axiom_order_def,zero_less_one,reals}.
+    Omitted.
 \end{proof}
 
 \begin{lemma}\label{negation_and_order}
     Suppose $r \in \reals$.
     $r \leq \zero$ iff $\zero \leq \neg{r}$.
 \end{lemma}
-
+\begin{proof}
+    Omitted.
+\end{proof}
 
 
 \begin{lemma}\label{reals_add_of_positiv}
@@ -548,7 +599,7 @@ Such that we can introduce the integers and raitionals as smooth as possible.
     Then $x + y$ is positiv.
 \end{lemma}
 \begin{proof}
-    
+    Omitted.
 \end{proof}
 
 \begin{lemma}\label{reals_mul_of_positiv}
-- 
cgit v1.2.3


From b8cc467735054bb3c38bf37b5e29877ba756c4b5 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 27 Aug 2024 20:20:46 +0200
Subject: working commit

---
 library/everything.tex        |  1 +
 library/topology/urysohn2.tex | 19 +++++++++++++++++++
 2 files changed, 20 insertions(+)

(limited to 'library/everything.tex')

diff --git a/library/everything.tex b/library/everything.tex
index b966197..94dd6d8 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -30,6 +30,7 @@
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
 \import{numbers.tex}
+\import{topology/urysohn2.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index ea49a6c..a64fa7e 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -16,6 +16,22 @@
 \section{Urysohns Lemma}
 
 
+\begin{definition}\label{one_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\end{definition}
+
+\begin{struct}\label{sequence}
+    A sequence $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\index$
+        \item $\indexset$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$.
+        \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$.
+    \end{enumerate}
+\end{struct}
 
 \begin{abbreviation}\label{urysohnspace}
     $X$ is a urysohn space iff
@@ -33,6 +49,7 @@
 
 
 
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
@@ -52,6 +69,8 @@
         % & x ,x \in X    <- will result in technicly ambigus parse
     \end{cases}
 
+
+    $U_1$
     Trivial.
     
     
-- 
cgit v1.2.3

