diff options
Diffstat (limited to 'library/topology')
| -rw-r--r-- | library/topology/continuous.tex | 14 | ||||
| -rw-r--r-- | library/topology/urysohn.tex | 274 |
2 files changed, 286 insertions, 2 deletions
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} |