1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
\import{topology/topological-space.tex}
\import{numbers.tex}
\import{function.tex}
\import{set/powerset.tex}
\section{Metric Spaces}
\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{definition}
\begin{definition}\label{open_ball}
$\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric on $M$ and $f(x,z) < r$ } \}$.
\end{definition}
\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.
\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_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}
\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.
For all $U,V \subseteq M$ if $U$, $V$ are open balls 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
% \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}
|
