diff options
| -rw-r--r-- | library/numbers.tex | 72 | ||||
| -rw-r--r-- | library/topology/metric-space.tex | 80 | ||||
| -rw-r--r-- | library/topology/order-topology.tex | 32 |
3 files changed, 146 insertions, 38 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index 93623fa..afb7d3f 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -4,6 +4,14 @@ \section{The real numbers} +%TODO: Implementing Notion for negativ number such as -x. + +%TODO: +%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher +%\cdot für multiklikation verwenden. +%< für die relation benutzen. + + \begin{signature} $\reals$ is a set. \end{signature} @@ -22,19 +30,31 @@ \begin{axiom}\label{reals_axiom_order} $\lt[\reals]$ is an order on $\reals$. - %$\reals$ is an ordered set. \end{axiom} \begin{axiom}\label{reals_axiom_strictorder} $\lt[\reals]$ is a strict order. \end{axiom} +\begin{abbreviation}\label{less_on_reals} + $x < y$ iff $(x,y) \in \lt[\reals]$. +\end{abbreviation} + +\begin{abbreviation}\label{greater_on_reals} + $x > y$ iff $y < x$. +\end{abbreviation} + +\begin{abbreviation}\label{lesseq_on_reals} + $x \leq y$ iff it is wrong that $x > y$. +\end{abbreviation} + +\begin{abbreviation}\label{greatereq_on_reals} + $x \geq y$ iff it is wrong that $x < y$. +\end{abbreviation} + \begin{axiom}\label{reals_axiom_dense} For all $x,y \in \reals$ if $(x,y)\in \lt[\reals]$ then there exist $z \in \reals$ such that $(x,z) \in \lt[\reals]$ and $(z,y) \in \lt[\reals]$. - - %For all $X,Y \subseteq \reals$ if for all $x,y$ $x\in X$ and $y \in Y$ such that $x \lt[\reals] y$ - %then there exist a $z \in \reals$ such that if $x \neq z$ and $y \neq z$ $x \lt[\reals] z$ and $z \lt[\reals] y$. \end{axiom} \begin{axiom}\label{reals_axiom_order_def} @@ -57,18 +77,12 @@ \begin{axiom}\label{reals_axiom_zero_in_reals} $\zero \in \reals$. \end{axiom} - -%\begin{axiom}\label{reals_axiom_one_in_reals} -% $\one \in \reals$. -%\end{axiom} - + \begin{axiom}\label{reals_axiom_zero} - %There exist $\zero \in \reals$ such that For all $x \in \reals$ $x + \zero = x$. \end{axiom} \begin{axiom}\label{reals_axiom_one} - %There exist $1 \in \reals$ such that For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$. \end{axiom} @@ -76,11 +90,6 @@ For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. \end{axiom} -%TODO: Implementing Notion for negativ number such as -x. - -%\begin{abbreviation}\label{reals_notion_minus} -% $y = -x$ iff $x + y = \zero$. -%\end{abbreviation} %This abbrevation result in a killed process. \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$. @@ -98,27 +107,8 @@ For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. \end{proposition} -\begin{signature} - $\invers$ is a set. -\begin{signature} - -%TODO: -%x \rless y in einer signatur hinzufügen und dann axiom x+z = y und dann \rlt in def per iff -%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher -%\cdot für multiklikation verwenden. -%< für die relation benutzen. - -%\begin{signature} -% $y^{\rightarrow}$ is a function. -%\end{signature} -%\begin{axiom}\label{notion_multi_invers} -% If $y \in \reals$ then $\invers{y} \in \reals$ and $y \times y^{\rightarrow} = 1$. -%\end{axiom} -%\begin{abbreviation}\label{notion_fraction} -% $\frac{x}{y} = x \times y^{\rightarrow}$. -%\end{abbreviation} \begin{lemma}\label{order_reals_lemma1} For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ @@ -138,3 +128,15 @@ if $(y,z) \in \lt[\reals]$ then $((x \times z), (x \times y)) \in \lt[\reals]$. \end{lemma} + +\begin{lemma}\label{a} + For all $x,y \in \reals$ if $x > y$ then $x \geq y$. +\end{lemma} + +\begin{lemma}\label{aa} + For all $x,y \in \reals$ if $x < y$ then $x \leq y$. +\end{lemma} + +\begin{lemma}\label{aaa} + For all $x,y \in \reals$ if $x \leq y \leq x$ then $x=y$. +\end{lemma}
\ No newline at end of file diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex new file mode 100644 index 0000000..7021a60 --- /dev/null +++ b/library/topology/metric-space.tex @@ -0,0 +1,80 @@ +\import{topology/topological-space.tex} +\import{numbers.tex} +\import{function.tex} + +\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 + $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} + +\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$ } \}$. +\end{definition} + + +\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_metric} $\metric[M]$ is a metric. + \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, 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$. +\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} + diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex index afa8755..2dd026d 100644 --- a/library/topology/order-topology.tex +++ b/library/topology/order-topology.tex @@ -1,7 +1,33 @@ \import{topology/topological-space.tex} +\import{order/order.tex} \section{Order Topology} -\begin{definition} - A -\end{definition} +\begin{abbreviation}\label{open_interval} + $z \in \oointervalof{x}{y}$ iff $x \mathrel{R} y$ and $x \mathrel{R} z$ and $z \mathrel{R} y$. + %$\oointervalof{x}{y}{X} = \{ z \mid x \in X, y \in X, z \in X x \mathrel{R} y \wedge x \mathrel{R} z \wedge z \mathrel{R} y\}$. +\end{abbreviation} + +\begin{struct}\label{order_topology} + A ordertopology space $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $<$ + \end{enumerate} + such that + \begin{enumerate} + \item \label{order_topology_1} $<$ is a strict order on $X$ + \item \label{order_topology_2} + \item \label{order_topology_3} + \item \label{order_topology_4} + \item \label{order_topology} + \item \label{order_topology} + \item \label{order_topology} + \end{enumerate} +\end{struct} + + + +%\begin{definition}\label{order_topology} +% $X$ has the order topology iff for all $x,y \in X$ $X$ has a strict order $R$ and $\oointervalof{x}{y}{X} \in \opens[X]$ and $X$ is a topological space. +% %$O$ is the order Topology on $X$ iff for all $x,y \in X$ $X$ has a strict order $R$ and $(x,y) \in O$ and $O$ is . +%\end{definition} |