formalisation mertic optimized

2 files changed, 38 insertions, 21 deletions

diff --git a/library/numbers.tex b/library/numbers.tex
index df47d81..a0e2211 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -10,7 +10,7 @@
 %\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher
 %\cdot für multiklikation verwenden. 
 %< für die relation benutzen.
-
+% sup und inf einfügen
 
 \begin{signature}
     $\reals$ is a set.
@@ -92,7 +92,7 @@
 
 
 \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$.
+    For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \times y = 1$.
 \end{axiom}
 
 \begin{axiom}\label{reals_axiom_disstro1}
@@ -107,7 +107,10 @@
     For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
 \end{proposition}
 
-
+\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{lemma}\label{order_reals_lemma1}
@@ -129,14 +132,15 @@
     then $(x \times z) < (x \times y)$.
 \end{lemma}
 
-\begin{lemma}\label{a}
+\begin{lemma}\label{o4rder_reals_lemma}
     For all $x,y \in \reals$ if $x > y$ then $x \geq y$.
 \end{lemma}
 
-\begin{lemma}\label{aa}
+\begin{lemma}\label{order_reals_lemma5}
     For all $x,y \in \reals$ if $x < y$ then $x \leq y$.
 \end{lemma}
 
-\begin{lemma}\label{aaa}
+\begin{lemma}\label{order_reals_lemma6}
     For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$.
-\end{lemma}
\ No newline at end of file
+\end{lemma}
+
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 7021a60..2a31d95 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,23 +4,22 @@
 
 \section{Metric Spaces}
 
-\begin{abbreviation}\label{metric}
-    $f$ is a metric iff $f$ is a function to $\reals$.
-\end{abbreviation}
-
-\begin{axiom}\label{metric_axioms}
-    $f$ is a metric iff $\dom{f} = A \times A$ and
-    for all $x,y,z \in A$ we have 
+\begin{definition}\label{metric}
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
+    for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
         $f(x,y) \leq f(x,z) + f(z,y)$ and
         if $x \neq y$ then $\zero < f(x,y)$.
-\end{axiom}
+\end{definition}
 
 \begin{definition}\label{open_ball}
-    $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric and $\dom{f} = M \times M$ and $f(x,z)<r$ } \}$.
+    $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric on $M$ and $f(x,z) < r$ } \}$.
 \end{definition}
 
+%TODO: \metric_opens{d} =  {hier die construction für topology}
+%TODO: Die induzierte topology definieren und dann in struct verwenden.
+
 
 \begin{struct}\label{metric_space}  
     A metric space $M$ is a onesorted structure equipped with
@@ -29,8 +28,7 @@
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item \label{metric_space_d}                        $\metric[M]$ is a function from $M \times M$ to $\reals$.
-        \item \label{metric_space_metric}                   $\metric[M]$ is a metric.
+        \item \label{metric_space_metric}                   $\metric[M]$ is a metric on $M$.
         \item \label{metric_space_topology}                 $M$ is a topological space.
         \item \label{metric_space_opens}                    for all $x \in M$ for all $r \in \reals$ $\openball{r}{x}{\metric[M]} \in \opens[M]$.
     \end{enumerate}
@@ -45,12 +43,27 @@
 \end{abbreviation}
 
 \begin{lemma}\label{union_of_open_balls_is_open}
-    Let $M$ be a metric space, let $U$ be an open ball in $M$, and let
-    $V$ be an open ball in $M$.
-    Then $U \union V$ is open in $M$.
+    Let $M$ be a metric space.
+    For all $U,V \subseteq M$ if $U$ is an open ball in $M$ and $V$ is an open ball in $M$ then $U \union V$ is open in $M$.
 \end{lemma}
 
 
+%\begin{definition}\label{lenght_of_interval} %TODO: take minus if its implemented
+%    $\lenghtinterval{x}{y} = r$ 
+%\end{definition}
+
+
+
+
+
+\begin{lemma}\label{metric_implies_topology}
+    Let $M$ be a set, and let $f$ be a metric on $M$.
+    Then $M$ is a metric space.
+\end{lemma}
+
+
+
+
 
 %\begin{struct}\label{metric_space}  
 %    A metric space $M$ is a onesorted structure equipped with