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

2 files changed, 38 insertions, 90 deletions

diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 6fa9fbd..bd7d15a 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -56,24 +56,52 @@
     $\emptyset \in \genOpens{B}{X}$.
 \end{lemma}
 
-\begin{lemma}\label{all_is_in_genopens}
+
+
+\begin{lemma}\label{union_in_genopens}
     Assume $B$ is a topological basis for $X$.
-    $X \in \genOpens{B}{X}$.
+    Assume $F\subseteq \genOpens{B}{X}$.
+    Then $\unions{F}\in\genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
-    $\unions{B} \in \genOpens{B}{X}$.
-    $X \subseteq \unions{B}$.
+    We have $\unions{F} \in \pow{X}$.
+
+    Show for all $x\in \unions{F}$ there exists $W \in B$
+    such that $x\in W$ and $W \subseteq \unions{F}$.
+    \begin{subproof}
+        Fix $x \in \unions{F}$.
+        There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}.
+        $V \in \genOpens{B}{X}$.
+        There exists $W \in B$ such that $x \in W \subseteq V$.
+        Then $W \subseteq \unions{F}$.
+    \end{subproof}
+    Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}.
 \end{proof}
 
-\begin{lemma}\label{union_in_genopens}
+\begin{lemma}\label{basis_is_in_genopens}
     Assume $B$ is a topological basis for $X$.
-    For all $F\subseteq \genOpens{B}{X}$ we have $\unions{F}\in\genOpens{B}{X}$.
+    $B \subseteq \genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    Omitted.
+    We show for all $V \in B$ $V \in \genOpens{B}{X}$.
+    \begin{subproof}
+        Fix $V \in B$.
+        For all $x \in V$ $x \in V \subseteq V$.
+        $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+        $V \in \pow{X}$.
+        $V \in \genOpens{B}{X}$.
+    \end{subproof}
 \end{proof}
 
+\begin{lemma}\label{all_is_in_genopens}
+    Assume $B$ is a topological basis for $X$.
+    $X \in \genOpens{B}{X}$.
+\end{lemma}
+\begin{proof}
+    $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+    $\unions{B} \in \genOpens{B}{X}$.
+    $X \subseteq \unions{B}$.
+\end{proof}
 
 \begin{lemma}\label{inters_in_genopens}
     Assume $B$ is a topological basis for $X$.
@@ -92,16 +120,13 @@
         Then $x\in A,C$.
         There exists $V'  \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}.
         There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}.
-        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$.
+        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$ by \cref{topological_basis}.
 
         Show $W \subseteq (A\inter C)$.
         \begin{subproof}
-            %$W \subseteq v'$ and $W \subseteq V''$.
             For all $y \in W$ we have $y \in V'$ and $y \in V''$.
         \end{subproof}
     \end{subproof}
-    %Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
-    %such that $x\in W$ and $W \subseteq (A\inter C)$.
 
-    $(A\inter C) \in \genOpens{B}{X}$.
+    $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}.
 \end{proof}
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.
-