diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/numbers.tex | 18 | ||||
| -rw-r--r-- | library/topology/metric-space.tex | 41 |
2 files changed, 38 insertions, 21 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index df47d81..a0e2211 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -10,7 +10,7 @@ %\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher %\cdot für multiklikation verwenden. %< für die relation benutzen. - +% sup und inf einfügen \begin{signature} $\reals$ is a set. @@ -92,7 +92,7 @@ \begin{axiom}\label{reals_axiom_mul_invers} - For all $x \in \reals$ there exist $y \in \reals$ such that $x \neq \zero$ and $x \times y = 1$. + For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \times y = 1$. \end{axiom} \begin{axiom}\label{reals_axiom_disstro1} @@ -107,7 +107,10 @@ For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{proposition} - +\begin{axiom}\label{reals_axiom_dedekind_complete} + For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$ + such that $x < z < y$. +\end{axiom} \begin{lemma}\label{order_reals_lemma1} @@ -129,14 +132,15 @@ then $(x \times z) < (x \times y)$. \end{lemma} -\begin{lemma}\label{a} +\begin{lemma}\label{o4rder_reals_lemma} For all $x,y \in \reals$ if $x > y$ then $x \geq y$. \end{lemma} -\begin{lemma}\label{aa} +\begin{lemma}\label{order_reals_lemma5} For all $x,y \in \reals$ if $x < y$ then $x \leq y$. \end{lemma} -\begin{lemma}\label{aaa} +\begin{lemma}\label{order_reals_lemma6} For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. -\end{lemma}
\ No newline at end of file +\end{lemma} + diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex index 7021a60..2a31d95 100644 --- a/library/topology/metric-space.tex +++ b/library/topology/metric-space.tex @@ -4,23 +4,22 @@ \section{Metric Spaces} -\begin{abbreviation}\label{metric} - $f$ is a metric iff $f$ is a function to $\reals$. -\end{abbreviation} - -\begin{axiom}\label{metric_axioms} - $f$ is a metric iff $\dom{f} = A \times A$ and - for all $x,y,z \in A$ we have +\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{axiom} +\end{definition} \begin{definition}\label{open_ball} - $\openball{r}{x}{f} = \{z \in M \mid \text{ $f$ is a metric and $\dom{f} = M \times M$ and $f(x,z)<r$ } \}$. + $\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 @@ -29,8 +28,7 @@ \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_metric} $\metric[M]$ is a metric. + \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} @@ -45,12 +43,27 @@ \end{abbreviation} \begin{lemma}\label{union_of_open_balls_is_open} - Let $M$ be a metric space, let $U$ be an open ball in $M$, and let - $V$ be an open ball in $M$. - Then $U \union V$ is open in $M$. + 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 |