path: root/library/topology/urysohn.tex

\import{topology/topological-space.tex}
\import{topology/separation.tex}
\import{topology/continuous.tex}
\import{topology/basis.tex}
\import{numbers.tex}
\import{function.tex}
\import{set.tex}
\import{cardinal.tex}
\import{relation.tex}
\import{relation/uniqueness.tex}
\import{set/cons.tex}
\import{set/powerset.tex}
\import{set/fixpoint.tex}
\import{set/product.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}



%%-----------------------
%   Idea:
%   A sequence could be define as a family of sets, 
%   together with the existence of an indexing function.
%
%%-----------------------
\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{minimum}
    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
\end{definition}

\begin{definition}\label{maximum}
    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
\end{definition}

\begin{definition}\label{intervalclosed}
    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
\end{definition}

\begin{definition}\label{intervalopen}
    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < 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$.
        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$.
        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ 
            such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. 
    \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{definition}\label{urysohnchain_without_cardinality}
    $C$ is a urysohnchain in $X$ iff
    $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 $C'$ is a urysohnchain in $X$
    and 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}

\begin{abbreviation}\label{two}
    $\two = \suc{1}$.
\end{abbreviation}

\begin{lemma}\label{two_in_reals}
    $\two \in \reals$.
\end{lemma}

\begin{lemma}\label{two_in_naturals}
    $\two \in \naturals$.
\end{lemma}

\begin{inductive}\label{power_of_two}
    Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$.
    \begin{enumerate}
        \item  $(\zero, 1) \in \powerOfTwoSet$.
        \item  If $(m,k) \in \powerOfTwoSet$, then $(m+1, k \rmul \two) \in \powerOfTwoSet$.
    \end{enumerate}
\end{inductive}

\begin{abbreviation}\label{pot}
    $\pot = \powerOfTwoSet$.
\end{abbreviation}

\begin{lemma}\label{dom_pot}
    $\dom{\pot} = \naturals$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{ran_pot}
    $\ran{\pot} \subseteq \naturals$.
\end{lemma}


\begin{axiom}\label{pot1}
    $\pot \in \funs{\naturals}{\naturals}$.
\end{axiom}

\begin{axiom}\label{pot2} 
    For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$.
    %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$.
\end{axiom}


%Without this abbreviation \pot cant be sed as a function in the standard sense
\begin{abbreviation}\label{pot_as_function}
    $\pot(n) = \apply{\pot}{n}$.
\end{abbreviation}


\begin{proposition}\label{urysohnchain_induction_begin}
    Let $X$ be a urysohn space.
    Suppose $A,B \in \closeds{X}$.
    Suppose $A \inter B$ is empty.
    Then there exist $U$
    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
    and $\indexset[U]= \{\zero, 1\}$
    and $\index[U](\zero) = A$
    and $\index[U](1) = (\carrier[X] \setminus B)$.
    %$U$ is a urysohnchain in $X$.
\end{proposition}
\begin{proof}

    Omitted.

    %   We show that $U$ is a sequence.
    %   \begin{subproof}
    %       Omitted.
    %   \end{subproof}
%   
    %   We show that $A \subseteq (\carrier[X] \setminus B)$.
    %   \begin{subproof}
    %       Omitted.
    %   \end{subproof}
%   
    %   We show that $U$ is a chain of subsets.
    %   \begin{subproof}
    %       For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
    %       It suffices to show that for all $n \in \indexset[U]$ we have
    %       for all $m \in \indexset[U]$ such that 
    %       $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
    %       Fix $n \in \indexset[U]$.
    %       Fix $m \in \indexset[U]$.
    %       \begin{byCase}
    %           \caseOf{$n = 1$.} Trivial.
    %           \caseOf{$n = \zero$.} 
    %               \begin{byCase}
    %                   \caseOf{$m = \zero$.} Trivial.
    %                   \caseOf{$m = 1$.} Omitted.
    %               \end{byCase}
    %       \end{byCase}
    %   \end{subproof}
%   
    %   $A \subseteq X$.
    %   $(X \setminus B) \subseteq X$.
    %   We show that for all $x \in U$ we have $x \subseteq X$.
    %   \begin{subproof}
    %       Omitted.
    %   \end{subproof}
%   
    %   We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$.
    %   \begin{subproof}
    %       Omitted.
    %   \end{subproof}
    %   We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
    %   $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
    %   \begin{subproof}
    %       Omitted.
    %   \end{subproof}

    
\end{proof}

\begin{proposition}\label{urysohnchain_induction_begin_step_two}
    Let $X$ be a urysohn space.
    Suppose $A,B \in \closeds{X}$.
    Suppose $A \inter B$ is empty.
    Suppose there exist $U$
    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
    and $\indexset[U]= \{\zero, 1\}$
    and $\index[U](\zero) = A$
    and $\index[U](1) = (\carrier[X] \setminus B)$.
    Then $U$ is a urysohnchain in $X$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}



\begin{proposition}\label{t_four_propositon}
    Let $X$ be a urysohn space.
    Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$
    we have there exists $C \subseteq X$ such that 
    $\closure{A}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{B}{X}$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}



\begin{proposition}\label{urysohnchain_induction_step_existence}
    Let $X$ be a urysohn space.
    Suppose $U$ is a urysohnchain in $X$.
    Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$.
\end{proposition}
\begin{proof}
    % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
    % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})

    % Let $m = \max{\indexset[U]}$.
    % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
    % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$.
    
    
    %\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}
    Omitted.

\end{proof}





\begin{proposition}\label{existence_of_staircase_function}
    Let $X$ be a urysohn space.
    Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
    Suppose $k \neq \zero$.
    Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
    and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ 
    we have $f(x) = \rfrac{n}{k}$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{abbreviation}\label{refinment_abbreviation}
    $x \refine y$ iff $x$ is a refinmant of $y$.
\end{abbreviation}





\begin{abbreviation}\label{sequence_of_functions}
    $f$ is a sequence of functions iff $f$ is a sequence 
    and for all $g \in \carrier[f]$ we have $g$ is a function.
\end{abbreviation}

\begin{abbreviation}\label{sequence_in_reals}
    $s$ is a sequence of real numbers iff $s$ is a sequence 
    and for all $r \in \carrier[s]$ we have $r \in \reals$.
\end{abbreviation}



\begin{axiom}\label{abs_behavior1}
    If $x \geq \zero$ then $\abs{x} = x$.
\end{axiom}

\begin{axiom}\label{abs_behavior2}
    If $x < \zero$ then $\abs{x} = \neg{x}$.
\end{axiom}

\begin{abbreviation}\label{converge}
    $s$ converges iff $s$ is a sequence of real numbers 
    and $\indexset[s]$ is infinite
    and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
    there exist $N \in \indexset[s]$ such that
    for all $m \in \indexset[s]$ such that $m > N$ 
    we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$.
\end{abbreviation}


\begin{definition}\label{limit_of_sequence}
    $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
    and $x \in \reals$ and 
    for all $\epsilon \in \reals$ such that $\epsilon > \zero$
    we have there exist $n \in \indexset[s]$ such that 
    for all $m \in \indexset[s]$ such that $m > n$ 
    we have $\abs{x - \index[s](n)} < \epsilon$.
\end{definition}

\begin{proposition}\label{existence_of_limit}
    Let $s$ be a sequence of real numbers.
    Then $s$ converges iff there exist $x \in \reals$ 
    such that $x$ is the limit of $s$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{definition}\label{limit_sequence}
    $x$ is the limit sequence of $f$ iff
    $x$ is a sequence and $\indexset[x] = \dom{f}$ and
    for all $n \in \indexset[x]$ we have
    $\index[x](n) = f(n)$.
\end{definition}

\begin{definition}\label{realsminus}
    $\realsminus = \{r \in \reals \mid r < \zero\}$.
\end{definition}

\begin{abbreviation}\label{realsplus}
    $\realsplus = \reals \setminus \realsminus$.
\end{abbreviation}

\begin{proposition}\label{intervalclosed_subseteq_reals}
    Suppose $a,b \in \reals$.
    Suppose $a < b$.
    Then $\intervalclosed{a}{b} \subseteq \reals$.
\end{proposition}



\begin{lemma}\label{fraction1}
    Let $x \in \reals$.
    Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{frection2}
    Suppose $a,b \in \reals$.
    Suppose $a < b$.
    Then $\intervalopen{a}{b}$ is infinite.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{frection3}
    Suppose $a \in \reals$.
    Suppose $a < \zero$.
    Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. 
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{fraction4}
    Suppose $a,b,\epsilon \in \reals$.
    Suppose $\epsilon > \zero$.
    $\abs{a - b} < \epsilon$ iff $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{fraction5}
    Suppose $a,b,\epsilon \in \reals$.
    Suppose $\epsilon > \zero$.
    $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$ iff $a \in \intervalopen{(b - \epsilon)}{(b + \epsilon)}$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{fraction6}
    Suppose $a,\epsilon \in \reals$.
    Suppose $\epsilon > \zero$.
    $\intervalopen{(a - \epsilon)}{(a + \epsilon)} = \{r \in \reals \mid (a - \epsilon) < r < (a + \epsilon)\} $.
\end{proposition}

\begin{abbreviation}\label{epsilonball}
    $\epsBall{a}{\epsilon}  = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
\end{abbreviation}

\begin{proposition}\label{fraction7}
    Suppose $a,\epsilon \in \reals$.
    Suppose $\epsilon > \zero$.
    Then there exist $b \in \rationals$ such that $b \in \epsBall{a}{\epsilon}$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}



 
%\begin{definition}\label{sequencetwo}
%   $Z$ is a sequencetwo iff  $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$.
%\end{definition}
%
%\begin{proposition}\label{sequence_existence}
%    Suppose $N \subseteq \naturals$.
%    Suppose $M \subseteq \naturals$.
%    Suppose $N = M$.
%    Then there exist $Z,f$ such that $f$ is a bijection from $N$ to $M$ and $Z=(N,f,M)$ and $Z$ is a sequencetwo.
%\end{proposition}
%\begin{proof}
%    Let $f(x) = x$ for $x \in N$.
%    Let $Z=(N,f,M)$.
%\end{proof}
%The proposition above and the definition prove false together with
% ordinal_subseteq_unions, omega_is_an_ordinal, powerset_intro, in_irrefl









\begin{theorem}\label{urysohn}
    Let $X$ be a urysohn space.
    Suppose $A,B \in \closeds{X}$.
    Suppose $A \inter B$ is empty.
    Suppose $\carrier[X]$ is inhabited.
    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
    and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
\end{theorem}
\begin{proof}
    
    There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
    and $\indexset[\eta] = \{\zero, 1\}$ 
    and $\index[\eta](\zero) = A$
    and $\index[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
    
    We show that there exist $\zeta$ such that $\zeta$ is a sequence 
    and $\indexset[\zeta] = \naturals$
    and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$
    and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ 
    and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$.
    \begin{subproof}
            %Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
            %Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
            %
            %    % TODO: Proof that \beta is a function which would be used for the indexing.
            %For all $n \in \naturals$ we have there exist $x \in \alpha$ such that $(n,x) \in \beta$.
            %$\dom{\beta} = \naturals$.
            %$\ran{\beta} = \alpha$.
            %$\beta \in \funs{\naturals}{\alpha}$.
            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$.
        Omitted.
    \end{subproof}

    Let $\alpha = \carrier[X]$.
    %Define $f : \alpha \to \naturals$ such that $f(x) =$
    %\begin{cases}
    %    & 1        & \text{if} x \in A \lor x \in B 
    %    & k     & \text{if} \exists k \in \naturals 
    %\end{cases}
%
    %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that
    %$k(x)$

    %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$.

    We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that for all $m \in \naturals$ we have $\pot(m) \in \naturals$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    
    We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
    and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ 
    we have $f(x) = \rfrac{n}{\pot(m)}$.
    \begin{subproof}
        Fix $m \in \indexset[\zeta]$.
        $\index[\zeta](m)$ is a urysohnchain in $X$.
        Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
        \begin{cases}
            & 0  & \text{if} x \in A 
            & 1 & \text{if} x \in B 
            & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1)
        \end{cases}

        
    \end{subproof}

    

    %The sequenc of the functions
    Let $\gamma = \{
        (n,f) \mid 
        n \in \naturals \mid 
        
        \forall n' \in \indexset[\index[\zeta](n)].             
        \forall x \in \carrier[X].      
        

        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land


        % (n,f) \in \gamma  <=>   \phi(n,f)
        % with \phi (n,f) :=        
        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 

            (       (n' = \zero)   
            \land   (x \in \index[\index[\zeta](n)](n')) 
            \land   (f(x)= \zero) ) 
        
        \lor
        
            (       (n' > \zero)    
            \land   (x \in \index[\index[\zeta](n)](n'))
            \land   (x \notin \index[\index[\zeta](n)](n'-1))
            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
            
        \lor

            (       (x \notin  \index[\index[\zeta](n)](n'))
            \land   (f(x) = 1) )
        
    \}$.
    
    Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.

    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
    is a function from $\carrier[X]$ to $\reals$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    
    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \index[\index[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
    \begin{subproof}
        Fix $n \in \naturals$.
        Fix $x \in \carrier[X]$.
    \end{subproof}



    We show that 
    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
    \begin{subproof}
        Omitted.
    \end{subproof} 



    We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that  $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
    \begin{subproof}       
        We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
        \begin{subproof}
            Fix $x \in \carrier[X]$.
            
            
            
            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
        \end{subproof}
    \end{subproof}
    

    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
    We have $\dom{G} = \carrier[X]$.

    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
    \begin{subproof}
        Fix $x \in \dom{G}$.
        It suffices to show that $g(x) \in \reals$.

        There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.

        We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$.
        \begin{subproof}
            Fix $\epsilon \in \reals$.
            

        \end{subproof}
        Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
    \end{subproof}

    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
    \begin{subproof}
        Fix $x \in \dom{G}$.
        Then $x \in \carrier[X]$.
        \begin{byCase}
            \caseOf{$x \in A$.} 
                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.


            \caseOf{$x \notin A$.} 
                \begin{byCase}
                    \caseOf{$x \in B$.} 
                        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.

                    \caseOf{$x \notin B$.}
                        Omitted.
                \end{byCase}
        \end{byCase}
    \end{subproof}


    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
    \begin{subproof}        
        It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
        It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$.
        Fix $x \in \dom{G}$.
        Then $x \in \carrier[X]$.
        $g(x) = G(x)$.
        We have $G(x) \in \reals$.
        $\zero \leq G(x) \leq 1$.
        We have $G(x) \in \intervalclosed{\zero}{1}$ .
    \end{subproof}

    We show that $G(A) = \zero$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that $G(B) = 1$.
    \begin{subproof}
        Omitted.
    \end{subproof}

    We show that $G$ is continuous.
    \begin{subproof}
        Omitted.
    \end{subproof}

    %Suppose $\eta$ is a urysohnchain in $X$.
    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
    %and $\indexset[\eta] = \{\zero, 1\}$
    %and $\index[\eta](\zero) = A$ 
    %and $\index[\eta](1) = (X \setminus B)$.


    %Then $\eta$ is a urysohnchain in $X$.

    %   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}