From 050b56baf7a158bff0eb721e03263b121bdc23c3 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Tue, 4 Jun 2024 11:19:21 +0200
Subject: Some notation fixes and lemma for topo basis generats opens was
 proofed and optimizised

---
 library/topology/metric-space.tex | 77 ---------------------------------------
 1 file changed, 77 deletions(-)

(limited to 'library/topology/metric-space.tex')

diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 1c6a0ca..bcc5b8c 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -21,44 +21,16 @@
 
 
 
-%\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$ and $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{definition}\label{metricopens}
     $\metricopens{d}{M} = \genOpens{\balls{d}{M}}{M}$.
 \end{definition}
 
 
-\begin{theorem}
-    Let $d$ be a metric on $M$.
-    $M$ is a topological space.
-\end{theorem}
-
 
 
 
@@ -93,13 +65,6 @@
 \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}
@@ -108,45 +73,3 @@
 \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}
-
-
-
-
-
-
-%TODO:  - Basis indudiert topology lemma
-%       - Offe Bälle sind basis
-
-% Was danach kommen soll bleibt offen, vll buch oder in proof wiki
-% Trennungsaxiom, 
-
-% Notaionen aufräumen damit das gut gemercht werden kann.
-
-- 
cgit v1.2.3