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

---
 library/numbers.tex | 140 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 140 insertions(+)
 create mode 100644 library/numbers.tex

(limited to 'library/numbers.tex')

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


From 3795588d157864a411baf2fc3afb31f9f5184d93 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 7 May 2024 14:41:15 +0200
Subject: Formalization of metric spaces and some cleaning of numbers.tex

Formalization of metric spaces:
Therefore we introduced the predicate metric and its axiomatization.
Then we introduced the term metric space in dependence of a metric function.
This metric space is automatically a a topological space.
---
 library/numbers.tex                 | 72 +++++++++++++++++----------------
 library/topology/metric-space.tex   | 80 +++++++++++++++++++++++++++++++++++++
 library/topology/order-topology.tex | 32 +++++++++++++--
 3 files changed, 146 insertions(+), 38 deletions(-)
 create mode 100644 library/topology/metric-space.tex

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index 93623fa..afb7d3f 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,6 +4,14 @@
 
 \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. 
+%< für die relation benutzen.
+
+
 \begin{signature}
     $\reals$ is a set.
 \end{signature}
@@ -22,19 +30,31 @@
 
 \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{abbreviation}\label{less_on_reals}
+    $x < y$ iff $(x,y) \in \lt[\reals]$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greater_on_reals}
+    $x > y$ iff $y < x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{lesseq_on_reals}
+    $x \leq y$ iff it is wrong that $x > y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greatereq_on_reals}
+    $x \geq y$ iff it is wrong that $x < y$.
+\end{abbreviation}
+
 \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}
@@ -57,18 +77,12 @@
 \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}
 
@@ -76,11 +90,6 @@
     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$.
@@ -98,27 +107,8 @@
     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]$ 
@@ -138,3 +128,15 @@
     if $(y,z) \in \lt[\reals]$ 
     then $((x \times z), (x \times y)) \in \lt[\reals]$.
 \end{lemma}
+
+\begin{lemma}\label{a}
+    For all $x,y \in \reals$ if $x > y$ then $x \geq y$.
+\end{lemma}
+
+\begin{lemma}\label{aa}
+    For all $x,y \in \reals$ if $x < y$ then $x \leq y$.
+\end{lemma}
+
+\begin{lemma}\label{aaa}
+    For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$.
+\end{lemma}
\ No newline at end of file
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
new file mode 100644
index 0000000..7021a60
--- /dev/null
+++ b/library/topology/metric-space.tex
@@ -0,0 +1,80 @@
+\import{topology/topological-space.tex}
+\import{numbers.tex}
+\import{function.tex}
+
+\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 
+        $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}
+
+\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$ } \}$.
+\end{definition}
+
+
+\begin{struct}\label{metric_space}  
+    A metric space $M$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\metric$
+    \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_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}
+\end{struct}
+
+\begin{abbreviation}\label{descriptive_syntax_for_openball1}
+    $U$ is an open ball in $M$ of $x$ with radius $r$ iff $x \in M$ and $M$ is a metric space and $U = \openball{r}{x}{\metric[M]}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{descriptive_syntax_for_openball2}
+    $U$ is an open ball in $M$ iff there exist $x \in M$ such that there exist $r \in \reals$ such that $U$ is an open ball in $M$ of $x$ with radius $r$.
+\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$.
+\end{lemma}
+
+
+
+%\begin{struct}\label{metric_space}  
+%    A metric space $M$ is a onesorted structure equipped with
+%    \begin{enumerate}
+%        \item $\metric$
+%    \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_distence_of_a_point}      $\metric[M](x,x) = \zero$.
+%        \item \label{metric_space_positiv}                  for all $x,y \in M$ if $x \neq y$ then $\zero < \metric[M](x,y)$.
+%        \item \label{metric_space_symetrie}                 $\metric[M](x,y) = \metric[M](y,x)$.
+%        \item \label{metric_space_triangle_equation}        for all $x,y,z \in M$ $\metric[M](x,y) < \metric[M](x,z) + \metric[M](z,y)$ or $\metric[M](x,y) = \metric[M](x,z) + \metric[M](z,y)$.
+%        \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$ $\{z \in M \mid \metric[M](x,z) < r\} \in \opens$.
+%    \end{enumerate}
+%\end{struct}
+
+%\begin{definition}\label{open_ball}
+%    $\openball{r}{x}{M} = \{z \in M \mid \metric(x,z) < r\}$.
+%\end{definition}
+
+%\begin{proposition}\label{open_ball_is_open}
+%    Let $M$ be a metric space,let $r \in \reals $, let $x$ be an element of $M$.
+%    Then $\openball{r}{x}{M} \in \opens[M]$.
+%\end{proposition}
+
diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex
index afa8755..2dd026d 100644
--- a/library/topology/order-topology.tex
+++ b/library/topology/order-topology.tex
@@ -1,7 +1,33 @@
 \import{topology/topological-space.tex}
+\import{order/order.tex}
 
 \section{Order Topology}
 
-\begin{definition}
-    A 
-\end{definition}
+\begin{abbreviation}\label{open_interval}
+    $z \in \oointervalof{x}{y}$ iff $x \mathrel{R} y$ and $x \mathrel{R} z$ and $z \mathrel{R} y$.
+    %$\oointervalof{x}{y}{X} = \{ z \mid x \in X, y \in X, z \in X x \mathrel{R} y \wedge x \mathrel{R} z \wedge z \mathrel{R} y\}$. 
+\end{abbreviation}
+
+\begin{struct}\label{order_topology}
+    A ordertopology space $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $<$
+    \end{enumerate}
+    such that 
+    \begin{enumerate}
+        \item \label{order_topology_1} $<$ is a strict order on $X$
+        \item \label{order_topology_2}  
+        \item \label{order_topology_3}
+        \item \label{order_topology_4}
+        \item \label{order_topology}
+        \item \label{order_topology}
+        \item \label{order_topology}
+    \end{enumerate}
+\end{struct}
+
+
+
+%\begin{definition}\label{order_topology}
+%    $X$ has the order topology iff for all $x,y \in X$ $X$ has a strict order $R$ and $\oointervalof{x}{y}{X} \in \opens[X]$ and $X$ is a topological space.
+%    %$O$ is the order Topology on $X$ iff for all $x,y \in X$ $X$ has a strict order $R$ and $(x,y) \in O$ and $O$ is . 
+%\end{definition}
-- 
cgit v1.2.3


From aeef2bd2dfc7e1a7f1865ee5455e934d9dedaa32 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 7 May 2024 14:50:35 +0200
Subject: Clean up of Notation in numbers.tex

First notation of tupels in the relation set was swapped with the canonical <.
---
 library/numbers.tex | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index afb7d3f..df47d81 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -53,16 +53,16 @@
 \end{abbreviation}
 
 \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 \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_order_def}
-    $(x,y) \in \lt[\reals]$ iff there exist $z \in \reals$ such that $(\zero, z) \in \lt[\reals]$ and $x + z = y$.
+    $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x + z = y$.
 \end{axiom}
 
 \begin{lemma}\label{reals_one_bigger_than_zero}
-    $(\zero,1) \in \lt[\reals]$.
+    $\zero < 1$.
 \end{lemma}
 
 
@@ -111,22 +111,22 @@
 
 
 \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]$.
+    For all $x,y,z \in \reals$ such that $\zero < x$ 
+    if $y < z$ 
+    then $(y \times x) < (z \times x)$.
 \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]$.
+    For all $x,y,z \in \reals$ such that $\zero < x$ 
+    if $y < z$ 
+    then $(x \times y) < (x \times z)$.
 \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]$.
+    For all $x,y,z \in \reals$ such that $x < \zero$ 
+    if $y < z$ 
+    then $(x \times z) < (x \times y)$.
 \end{lemma}
 
 \begin{lemma}\label{a}
-- 
cgit v1.2.3


From 08019dcdaf3b13bb8ce554dfd5377690bb508c6d Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 7 May 2024 18:08:04 +0200
Subject: formalisation mertic optimized

---
 library/numbers.tex               | 18 ++++++++++-------
 library/topology/metric-space.tex | 41 ++++++++++++++++++++++++++-------------
 2 files changed, 38 insertions(+), 21 deletions(-)

(limited to 'library/numbers.tex')

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


From 63518b2e0bfdf0308fba30920a7a3bb7f61da994 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 14 May 2024 16:55:40 +0200
Subject: work on metric spaces

---
 library/numbers.tex               | 49 +++++++++++++++++++++++++++++++++++++++
 library/topology/metric-space.tex | 45 +++++++++++++++++++++++++++++++++--
 2 files changed, 92 insertions(+), 2 deletions(-)

(limited to 'library/numbers.tex')

diff --git a/library/numbers.tex b/library/numbers.tex
index a0e2211..5dd06da 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -144,3 +144,52 @@
     For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$.
 \end{lemma}
 
+\begin{axiom}\label{reals_axiom_minus}
+    For all $x \in \reals$ $x - x = \zero$.
+\end{axiom}
+
+\begin{lemma}\label{reals_minus}
+    Assume $x,y \in \reals$. If $x - 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}
+
+\begin{definition}\label{least_upper_bound}
+    $x$ is a least upper bound of $X$ iff $x$ is an upper bound of $X$ and for all $y$ such that $y$ is an upper bound of $X$ we have $x \leq y$.
+\end{definition}
+
+\begin{lemma}\label{supremum_unique}
+    %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$.
+    If $x$ is a least upper bound of $X$ and $y$ is a least upper bound of $X$ then $x = y$.
+\end{lemma}
+
+\begin{definition}\label{supremum_reals}
+    $x$ is the supremum of $X$ iff $x$ is a least upper bound of $X$.
+\end{definition}
+
+
+
+
+\begin{definition}\label{lower_bound}
+    $x$ is an lower bound of $X$ iff for all $y \in X$ we have $x < y$.
+\end{definition}
+
+\begin{definition}\label{greatest_lower_bound}
+    $x$ is a greatest lower bound of $X$ iff $x$ is an lower bound of $X$ and for all $y$ such that $y$ is an lower bound of $X$ we have $x \geq y$.
+\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}
+
+\begin{definition}\label{infimum_reals}
+    $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
+\end{definition}
+
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 2a31d95..8ec83f7 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -1,6 +1,7 @@
 \import{topology/topological-space.tex}
 \import{numbers.tex}
 \import{function.tex}
+\import{set/powerset.tex}
 
 \section{Metric Spaces}
 
@@ -17,7 +18,46 @@
     $\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}
+
+
+\begin{definition}\label{induced_topology}
+    $O$ is the induced topology of $d$ in $M$ iff 
+    $O \subseteq \pow{M}$ and
+    $d$ is a metric on $M$ and 
+    for all $x,r,A,B,C$ 
+        such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$
+        we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$.
+\end{definition}
+
+%\begin{definition}
+%    $\projcetfirst{A} = \{a \mid \exists x \in X \text{there exist $x \i }  \}$
+%\end{definition}
+
+\begin{definition}\label{set_of_balls}
+    $\balls{d}{M} = \{ O \in \pow{M} \mid \text{there exists $x,r$ such that $r \in \reals$ and $x \in M$ we have $O = \openball{r}{x}{d}$ } \}$.
+\end{definition}
+
+
+\begin{definition}\label{toindsas}
+    $\metricopens{d}{M} = \{O \in \pow{M} \mid \text{
+        $d$ is a metric on $M$ and
+        for all $x,r,A,B,C$ 
+        such that $x \in M$ and $r \in \reals$ and $A,B \in O$ and $C$ is a family of subsets of $O$
+        we have $\openball{r}{x}{d} \in O$ and $\unions{C} \in O$ and $A \inter B \in O$.
+    }  \}$.
+    
+\end{definition}
+
+\begin{theorem}\label{metric_induce_a_topology}
+    
+
+
+\end{theorem}
+
+
+
+
+%TODO: \metric_opens{d} =  {hier die construction für topology} DONE.
 %TODO: Die induzierte topology definieren und dann in struct verwenden.
 
 
@@ -44,7 +84,7 @@
 
 \begin{lemma}\label{union_of_open_balls_is_open}
     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$.
+    For all $U,V \subseteq M$ if $U$, $V$ are open balls in $M$ then $U \union V$ is open in $M$.
 \end{lemma}
 
 
@@ -56,6 +96,7 @@
 
 
 
+
 \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.
-- 
cgit v1.2.3