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
|
\import{topology/topological-space.tex}
\import{numbers.tex}
\import{function.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}
%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
\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$ 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
% \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}
|
