Some notation fixes and lemma for topo basis generats opens was proofed and optimizised

1 files changed, 17 insertions, 24 deletions

diff --git a/library/numbers.tex b/library/numbers.tex
index 5dd06da..2451730 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,8 +4,6 @@
 
 \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. 
@@ -17,11 +15,11 @@
 \end{signature}
 
 \begin{signature}
-    $x + y$ is a set.
+    $x \add y$ is a set.
 \end{signature}
 
 \begin{signature}
-    $x \times y$ is a set.
+    $x \rmul y$ is a set.
 \end{signature}
 
 \begin{axiom}\label{one_in_reals}
@@ -58,7 +56,7 @@
 \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$.
+    $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x \add z = y$.
 \end{axiom}
 
 \begin{lemma}\label{reals_one_bigger_than_zero}
@@ -67,11 +65,11 @@
 
 
 \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)$.
+    For all $x,y,z \in \reals$ $(x \add y) \add z = x \add (y \add 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 \times y = y \times x$.
+    For all $x,y \in \reals$ $x \add y = y \add x$ and $x \rmul y = y \rmul x$.
 \end{axiom}
 
 \begin{axiom}\label{reals_axiom_zero_in_reals}
@@ -79,32 +77,32 @@
 \end{axiom}
   
 \begin{axiom}\label{reals_axiom_zero}
-    For all $x \in \reals$ $x + \zero = x$. 
+    For all $x \in \reals$ $x \add \zero = x$. 
 \end{axiom}
 
 \begin{axiom}\label{reals_axiom_one}
-    For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$.
+    For all $x \in \reals$ $1 \neq \zero$ and $x \rmul 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$.
+    For all $x \in \reals$ there exist $y \in \reals$ such that $x \add 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$.
+    For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul 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)$.
+    For all $x,y,z \in \reals$ $x \rmul (y \add z) = (x \rmul y) \add (x \rmul 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)$.
+    For all $x,y,z \in \reals$ $(y \add z) \rmul x = (y \rmul x) \add (z \rmul 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$.
+    For all $x,y,z \in \reals$ if $x \add y = x \add z$ then $y = z$.
 \end{proposition}
 
 \begin{axiom}\label{reals_axiom_dedekind_complete}
@@ -116,20 +114,20 @@
 \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)$.
+    then $(y \rmul x) < (z \rmul 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)$.
+    then $(x \rmul y) < (x \rmul 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)$.
+    then $(x \rmul z) < (x \rmul y)$.
 \end{lemma}
 
 \begin{lemma}\label{o4rder_reals_lemma}
@@ -145,17 +143,13 @@
 \end{lemma}
 
 \begin{axiom}\label{reals_axiom_minus}
-    For all $x \in \reals$ $x - x = \zero$.
+    For all $x \in \reals$ $x \rmiuns x = \zero$.
 \end{axiom}
 
 \begin{lemma}\label{reals_minus}
-    Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$.
+    Assume $x,y \in \reals$. If $x \rmiuns 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}
@@ -185,7 +179,6 @@
 \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}