diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/numbers.tex | 131 | ||||
| -rw-r--r-- | library/topology/continuous.tex | 14 | ||||
| -rw-r--r-- | library/topology/urysohn.tex | 274 |
3 files changed, 360 insertions, 59 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index 0bfae2d..7d1b058 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -348,6 +348,9 @@ We seen before that we can proof the common behavior of the naturals. Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals. Such that we can introduce the integers and raitionals as smooth as possible. + + +The operations Multiplication and addition is closed in the reals \begin{axiom}\label{reals_rmul} For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$. \end{axiom} @@ -358,10 +361,16 @@ Such that we can introduce the integers and raitionals as smooth as possible. + +Commutivatiy of the standart operations \begin{axiom}\label{reals_axiom_kommu} For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$. \end{axiom} + + + +Existence of one and Zero \begin{axiom}\label{reals_axiom_zero} For all $x \in \reals$ $x + \zero = x$. \end{axiom} @@ -370,6 +379,9 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x \in \reals$ we have $x \rmul 1 = x$. \end{axiom} + + +The Existence of Inverse of both operations \begin{axiom}\label{reals_axiom_add_invers} For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. \end{axiom} @@ -378,6 +390,9 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$. \end{axiom} + + +Disstrubitiv Laws of the reals \begin{axiom}\label{reals_axiom_disstro1} For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$. \end{axiom} @@ -386,10 +401,9 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$. \end{axiom} -\begin{axiom}\label{reals_reducion_on_addition} - For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. -\end{axiom} + +Definition of the order symbols \begin{abbreviation}\label{rless} $x < y$ iff $x \rless y$. \end{abbreviation} @@ -406,50 +420,50 @@ Such that we can introduce the integers and raitionals as smooth as possible. $x \geq y$ iff it is wrong that $x < y$. \end{abbreviation} + + +Laws of the order on the reals \begin{abbreviation}\label{is_positiv} $x$ is positiv iff $x > \zero$. \end{abbreviation} - - - - -\begin{axiom}\label{tarski1} +\begin{axiom}\label{reals_order} For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$. \end{axiom} -\begin{axiom}\label{tarski2} +\begin{axiom}\label{reals_dense} For all $x,y \in \reals$ if $x < y$ then there exist $z \in \reals$ such that $x < z$ and $z < y$. \end{axiom} -\begin{axiom}\label{tarski3} +\begin{axiom}\label{reals_is_eta_zero_set} 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{axiom}\label{tarski4} - For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$. +\begin{axiom}\label{reals_one_bigger_zero} + $\zero < 1$. \end{axiom} -\begin{axiom}\label{tarski5} - For all $x,y \in \reals$ we have there exist $z \in \reals$ such that $x + z = y$. +\begin{axiom}\label{reals_order_behavior_with_addition} + For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$. \end{axiom} - -\begin{axiom}\label{tarski8} - $\zero < 1$. +\begin{axiom}\label{reals_postiv_mul_is_positiv} + For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. \end{axiom} -\begin{axiom}\label{labelordersossss} - For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$. +\begin{axiom}\label{reals_postiv_mul_negativ_is_negativ} + For all $x,y \in \reals$ such that $x < \zero < y$ we have $(x \rmul y) < \zero$. \end{axiom} -\begin{axiom}\label{nocheinschoeneslabel} - For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. +\begin{axiom}\label{reals_negativ_mul_is_negativ} + For all $x,y \in \reals$ such that $x,y < \zero$ we have $\zero < (x \rmul y)$. \end{axiom} + + \subsection{The Intergers} @@ -480,10 +494,11 @@ Such that we can introduce the integers and raitionals as smooth as possible. For all $r \in \reals$ we have $\neg{\neg{r}} = r$. \end{proposition} \begin{proof} - Fix $r \in \reals$. - $r + \neg{r} = \zero$. - $\neg{r} + \neg{\neg{r}} = \zero$. - Follows by \cref{reals_reducion_on_addition,neg,reals_axiom_kommu}. + Omitted. +% Fix $r \in \reals$. +% $r + \neg{r} = \zero$. +% $\neg{r} + \neg{\neg{r}} = \zero$. +% Follows by \cref{neg,reals_axiom_kommu}. \end{proof} \begin{definition}\label{integers} @@ -511,22 +526,6 @@ Such that we can introduce the integers and raitionals as smooth as possible. -\begin{proposition}\label{integers_negativ_times_negativ_is_positiv} - Suppose $n,m \in \integers$. - Suppose $n < \zero$ and $m < \zero$. - Then $n \rmul m > \zero$. -\end{proposition} -\begin{proof} - Omitted. - %$n \neq \zero$ and $m \neq \zero$. - %For all $k \in \naturals$ we have $k = \zero \lor k > \zero$. - %There exists $n' \in \reals$ such that $n' + n = \zero$. - %There exists $m' \in \reals$ such that $m' + m = \zero$. -\end{proof} - -%TODO: negativ * negativ = positiv. - - \subsection{The Rationals} \begin{axiom}\label{invers_reals} @@ -542,7 +541,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. \end{abbreviation} \begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen - $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in \naturalsPlus. q = \rfrac{z}{n} \}$. + $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in (\integers \setminus \{\zero\}). q = \rfrac{z}{n} \}$. \end{definition} \begin{abbreviation}\label{nominator} @@ -553,23 +552,41 @@ Such that we can introduce the integers and raitionals as smooth as possible. $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$. \end{abbreviation} -%\begin{proposition}\label{q_is_less_then_p_if_denominator_is_bigger_and_nominator_is_equal} -% Suppose $p,q \in \rationals$. -% Suppose $z \in \naturals$. -% Suppose $p$ is positiv. -% Suppose $q$ is positiv. -% Suppose $z$ is nominator of $p$. -% Suppose $z$ is nominator of $p$. -% Suppose $p'$ is denominator of $p$. -% Suppose $q'$ is denominator of $q$. -% Then $p \leq q$ iff $p' \geq q'$. -%\end{proposition} +\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one} + For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$. +\end{theorem} +\begin{proof} + Omitted. +\end{proof} +\begin{lemma}\label{fraction_kuerzung} %TODO: Englischen namen rausfinden + For all $n,m,k \in \reals$ we have $\rfrac{n \rmul k}{m \rmul k} = \rfrac{n}{m}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} -%\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one} -% For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$. -%\end{theorem} +\begin{lemma}\label{fraction_swap} + For all $n,m,k,l \in \reals$ we have $\rfrac{\rfrac{n}{m}}{\rfrac{k}{l}}=\rfrac{n \rmul l}{m \rmul k}$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} +\begin{definition}\label{divisor} + $g$ is a integral divisor of $a$ iff $g \in \naturals$ and there exist $b \in \integers$ such that $g \rmul b = a$. +\end{definition} + + + + +%\begin{abbreviation}\label{gcd} +% $g$ is greatest common divisor of $\{a,b\}$ iff +% $g$ is a integral divisor of $a$ +% and $g$ is a integral divisor of $b$ +% and for all $g'$ such that $g'$ is a integral divisor of $a$ +% and $g'$ is a integral divisor of $b$ we have $g' \leq g$. +%\end{abbreviation} % TODO: Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, @@ -652,7 +669,7 @@ Such that we can introduce the integers and raitionals as smooth as possible. \begin{lemma}\label{order_reals_lemma3} Let $x,y,z \in \reals$. - Suppose $\zero < x$. + Suppose $\zero > x$. Suppose $y < z$. Then $(x \rmul z) < (x \rmul y)$. \end{lemma} diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex index 6a32353..a9bc58e 100644 --- a/library/topology/continuous.tex +++ b/library/topology/continuous.tex @@ -1,5 +1,7 @@ \import{topology/topological-space.tex} \import{relation.tex} +\import{function.tex} +\import{set.tex} \begin{definition}\label{continuous} $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$. @@ -8,18 +10,25 @@ \begin{proposition}\label{continuous_definition_by_closeds} Let $X$ be a topological space. Let $Y$ be a topological space. + Let $f \in \funs{X}{Y}$. Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. \end{proposition} \begin{proof} Omitted. - %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. + %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ such that $U \neq \emptyset$ we have $\preimg{f}{U} \in \closeds{X}$. %\begin{subproof} % Suppose $f$ is continuous. % Fix $U \in \closeds{Y}$. % $\carrier[Y] \setminus U$ is open in $Y$. % Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$. % Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$. - % $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % We show that $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % \begin{subproof} + % It suffices to show that for all $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ we have $x \in \preimg{f}{U}$. + % Fix $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. + % Take $y \in \carrier[Y]$ such that $f(x)=y$. + % It suffices to show that $y \in U$. + % \end{subproof} % $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. %\end{subproof} %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous. @@ -27,3 +36,4 @@ % Omitted. %\end{subproof} \end{proof} + diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex new file mode 100644 index 0000000..65457ea --- /dev/null +++ b/library/topology/urysohn.tex @@ -0,0 +1,274 @@ +\import{topology/topological-space.tex} +\import{topology/separation.tex} +\import{topology/continuous.tex} +\import{numbers.tex} +\import{function.tex} +\import{set.tex} +\import{cardinal.tex} + +\section{Urysohns Lemma} +% In this section we want to proof Urysohns lemma. +% We try to follow the proof of Klaus Jänich in his book. TODO: Book reference +% The Idea is to construct staircase functions as a chain. +% The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$. +% With the property that \[f\mid_{A}=1 \land f\mid_{B}=0\] for \[A,B\] closed sets. + +%Chains of sets. + +The first tept will be a formalisation of chain constructions. + +\subsection{Chains of sets} +% Assume $A,B$ are subsets of a topological space $X$. + +% As Jänich propose we want a special property on chains of subsets. +% We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. +% \begin{align} +% A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B +% \end{align} +% such that for all elements in this chain following holds, +% $\overline{A_{i-1}} \subset \interior{A_{i}}$. +% In this case we call the chain legal. + +\begin{definition}\label{one_to_n_set} + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. +\end{definition} + +\begin{definition}\label{cardinality} + $X$ has cardinality of $n$ iff + $n \in \naturals$ and there exists $b$ such that $b$ is a bijection from $\seq{1}{n}$ to $X$. +\end{definition} + + + +\begin{struct}\label{sequence} + A sequence $X$ is a onesorted structure equipped with + \begin{enumerate} + \item $\index$ + \item $\indexset$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. + \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{cahin_of_subsets} + $C$ is a chain of subsets iff + $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$. +\end{definition} + +\begin{definition}\label{chain_of_n_subsets} + $C$ is a chain of $n$ subsets iff + $C$ is a chain of subsets and $n \in \indexset[C]$ + and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$. +\end{definition} + + + +% TODO: The Notion above should be generalised to sequences since we need them as well for our limit +% and also for the subproof of continuity of the limit. + + +% \begin{definition}\label{legal_chain} +% $C$ is a legal chain of subsets of $X$ iff +% $C \subseteq \pow{X}$. %and +% %there exist $f \in \funs{C}{\naturals}$ such that +% %for all $x,y \in C$ we have if $f(x) < f(y)$ then $x \subset y \land \closure{x} \subset \interior{y}$. +% \end{definition} + +% TODO: We need a notion for declarinf new properties to existing thing. +% +% The following gives a example and a wish want would be nice to have: +% "A (structure) is called (adjectiv of property), if" +% +% This should then be use als follows: +% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). +% Which should be translated to fol like this: +% ?[X]: is_structure(X) & is_adjectiv_1(X) & ... & is_adjectiv_n(X) +% --------------------------------------------------------------- + + + +\subsection{staircase function} + +\begin{definition}\label{intervalclosed} + $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. +\end{definition} + + +\begin{struct}\label{staircase_function} + A staircase function $f$ is a onesorted structure equipped with + \begin{enumerate} + \item $\chain$ + \end{enumerate} + such that + \begin{enumerate} + \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$. + \item \label{staircase_domain} $\dom{f}$ is a topological space. + \item \label{staricase_def_chain} $C$ is a chain of subsets. + \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. + \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. + \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. + \end{enumerate} +\end{struct} + +\begin{definition}\label{legal_staircase} + $f$ is a legal staircase function iff + $f$ is a staircase function and + for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$. +\end{definition} + +\begin{abbreviation}\label{urysohnspace} + $X$ is a urysohn space iff + $X$ is a topological space and + for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$ + we have there exist $A',B' \in \opens[X]$ + such that $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$. +\end{abbreviation} + +\begin{definition}\label{urysohnchain} + $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused! + $C$ is a chain of subsets and + for all $A \in C$ we have $A \subseteq X$ and + for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. +\end{definition} + +\begin{abbreviation}\label{infinte_sequence} + $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite. +\end{abbreviation} + +\begin{definition}\label{infinite_product} + $X$ is the infinite product of $Y$ iff + $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$. +\end{definition} + +\begin{definition}\label{refinmant} + $C$ is a refinmant of $C'$ iff for all $x \in C'$ we have $x \in C$ and + for all $y \in C'$ such that $y \subset x$ we have there exist $c \in C$ such that $y \subset c \subset x$ + and for all $g \in C$ such that $g \neq c$ we have not $y \subset g \subset x$. +\end{definition} + + +% The next thing we need to define is the uniform staircase function. +% This function has it's domain in $X$ and maps to the closed interval $[0,1]$. +% These functions should behave als follows, +% \begin{align} +% &f(A_{0}) = 1 &\text{consant} \\ +% &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.} +% \end{align} + +% We then prove that for any given $r$ we find a repolished chain, +% which contains the $A_{i}$ and this replished chain is also legal. +% +% The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ +% be a staircase function with $n$ many refinemants. +% This limit will be continuous and we would be done. + + +% TODO: Since we want to prove that $f$ is continus, we have to formalize that +% \reals with the usual topology is a topological space. +% ------------------------------------------------------------- + +\begin{theorem}\label{urysohn} + Let $X$ be a urysohn space. + Suppose $A,B \subseteq \closeds{X}$. + Suppose $A \inter B$ is empty. + There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. +\end{theorem} +\begin{proof} + We show that for all $n \in \naturals$ we have + if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ + then there exist $C'$ such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ + and $C'$ is a refinmant of $C$. + \begin{subproof} + Omitted. + \end{subproof} + + + + Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. + + We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence + and for all $i \in \indexset[\zeta]$ we have + $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ + and $A \subseteq \index[\zeta](i)$ + and $\index[\zeta](i) \subseteq (X \setminus B)$ + and for all $j \in \indexset[\zeta]$ such that + $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. + \begin{subproof} + Omitted. + \end{subproof} + + + + + + + + + We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} + $g$ is a staircase function and $\chain[g] = C$. + $g$ is a legal staircase function. + + + We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. + \begin{subproof} + Omitted. + \end{subproof} + + + %We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. + %\begin{subproof} + % Omitted. + %\end{subproof} + + %Proof Sheme Idea: + % -We proof for n=1 that C_{n} is a chain and legal + % -Then by induction with P(n+1) is refinmant of P(n) + % -Therefore we have a increing refinmant of these Chains such that our limit could even apply + % --------------------------------------------------------- + + %We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function + %\begin{subproof} + % Omitted. + %\end{subproof} + + + % Formalization idea of enumarted sequences: + % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} + % - This should give all finite and infinte enumarable sequences + % - Introduce a notion for the indexing of these enumarable sequences. + % - Then we can define the limit of a enumarted sequence of functions. + % --------------------------------------------------------- + % + % Here we need a limit definition for sequences of functions + %We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$ + %\begin{subproof} + % Omitted. + %\end{subproof} + % + %We show that $F(A) = 1$. + %\begin{subproof} + % Omitted. + %\end{subproof} + % + %We show that $F(B) = 0$. + %\begin{subproof} + % Omitted. + %\end{subproof} + % + %We show that $F$ is continuous. + %\begin{subproof} + % Omitted. + %\end{subproof} +\end{proof} + +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} |