diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/numbers.tex | 41 | ||||
| -rw-r--r-- | library/topology/basis.tex | 51 | ||||
| -rw-r--r-- | library/topology/metric-space.tex | 77 |
3 files changed, 55 insertions, 114 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index 5dd06da..2451730 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -4,8 +4,6 @@ \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. @@ -17,11 +15,11 @@ \end{signature} \begin{signature} - $x + y$ is a set. + $x \add y$ is a set. \end{signature} \begin{signature} - $x \times y$ is a set. + $x \rmul y$ is a set. \end{signature} \begin{axiom}\label{one_in_reals} @@ -58,7 +56,7 @@ \end{axiom} \begin{axiom}\label{reals_axiom_order_def} - $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x + z = y$. + $x < y$ iff there exist $z \in \reals$ such that $\zero < z$ and $x \add z = y$. \end{axiom} \begin{lemma}\label{reals_one_bigger_than_zero} @@ -67,11 +65,11 @@ \begin{axiom}\label{reals_axiom_assoc} - For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \times y) \times z = x \times (y \times z)$. + For all $x,y,z \in \reals$ $(x \add y) \add z = x \add (y \add z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$. \end{axiom} \begin{axiom}\label{reals_axiom_kommu} - For all $x,y \in \reals$ $x + y = y + x$ and $x \times y = y \times x$. + For all $x,y \in \reals$ $x \add y = y \add x$ and $x \rmul y = y \rmul x$. \end{axiom} \begin{axiom}\label{reals_axiom_zero_in_reals} @@ -79,32 +77,32 @@ \end{axiom} \begin{axiom}\label{reals_axiom_zero} - For all $x \in \reals$ $x + \zero = x$. + For all $x \in \reals$ $x \add \zero = x$. \end{axiom} \begin{axiom}\label{reals_axiom_one} - For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$. + For all $x \in \reals$ $1 \neq \zero$ and $x \rmul 1 = x$. \end{axiom} \begin{axiom}\label{reals_axiom_add_invers} - For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. + For all $x \in \reals$ there exist $y \in \reals$ such that $x \add y = \zero$. \end{axiom} \begin{axiom}\label{reals_axiom_mul_invers} - For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \times y = 1$. + For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$. \end{axiom} \begin{axiom}\label{reals_axiom_disstro1} - For all $x,y,z \in \reals$ $x \times (y + z) = (x \times y) + (x \times z)$. + For all $x,y,z \in \reals$ $x \rmul (y \add z) = (x \rmul y) \add (x \rmul z)$. \end{axiom} \begin{proposition}\label{reals_disstro2} - For all $x,y,z \in \reals$ $(y + z) \times x = (y \times x) + (z \times x)$. + For all $x,y,z \in \reals$ $(y \add z) \rmul x = (y \rmul x) \add (z \rmul x)$. \end{proposition} \begin{proposition}\label{reals_reducion_on_addition} - For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. + For all $x,y,z \in \reals$ if $x \add y = x \add z$ then $y = z$. \end{proposition} \begin{axiom}\label{reals_axiom_dedekind_complete} @@ -116,20 +114,20 @@ \begin{lemma}\label{order_reals_lemma1} For all $x,y,z \in \reals$ such that $\zero < x$ if $y < z$ - then $(y \times x) < (z \times x)$. + then $(y \rmul x) < (z \rmul x)$. \end{lemma} \begin{lemma}\label{order_reals_lemma2} For all $x,y,z \in \reals$ such that $\zero < x$ if $y < z$ - then $(x \times y) < (x \times z)$. + then $(x \rmul y) < (x \rmul z)$. \end{lemma} \begin{lemma}\label{order_reals_lemma3} For all $x,y,z \in \reals$ such that $x < \zero$ if $y < z$ - then $(x \times z) < (x \times y)$. + then $(x \rmul z) < (x \rmul y)$. \end{lemma} \begin{lemma}\label{o4rder_reals_lemma} @@ -145,17 +143,13 @@ \end{lemma} \begin{axiom}\label{reals_axiom_minus} - For all $x \in \reals$ $x - x = \zero$. + For all $x \in \reals$ $x \rmiuns x = \zero$. \end{axiom} \begin{lemma}\label{reals_minus} - Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$. + Assume $x,y \in \reals$. If $x \rmiuns y = \zero$ then $x=y$. \end{lemma} -%\begin{definition}\label{reasl_supremum} %expaction "there exists" after \mid -% $\rsup{X} = \{z \mid \text{ $z \in \reals$ and for all $x,y$ such that $x \in X$ and $y,x \in \reals$ and $x < y$ we have $z \leq y$ }\}$. -%\end{definition} - \begin{definition}\label{upper_bound} $x$ is an upper bound of $X$ iff for all $y \in X$ we have $x > y$. \end{definition} @@ -185,7 +179,6 @@ \end{definition} \begin{lemma}\label{infimum_unique} - %Let $x,y \in \reals$ and let $X$ be a subset of $\reals$. If $x$ is a greatest lower bound of $X$ and $y$ is a greatest lower bound of $X$ then $x = y$. \end{lemma} 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. - |