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(-)

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