path: root/library/topology/urysohn2.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}
\import{topology/real-topological-space.tex}

\section{Urysohns Lemma}




\begin{definition}\label{sequence}
    $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$.
\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{abbreviation}\label{at}
    $\at{f}{n} = f(n)$.
\end{abbreviation}


\begin{definition}\label{chain_of_subsets}
    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
\end{definition}


\begin{definition}\label{urysohnchain}%<-- zulässig
    $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$.
\end{definition}

\begin{definition}\label{urysohn_finer_set}
    $A$ is finer between $X$ to $Y$ in $U$ iff $\closure{X}{U} \subseteq \interior{A}{U}$ and $\closure{A}{U} \subseteq \interior{Y}{U}$.
\end{definition}

\begin{definition}\label{finer} %<-- verfeinerung 
    $Y$ is finer then $X$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $\at{Y}{k}$ is finer between $\at{X}{n}$ to $\at{X}{m}$ in $U$.
\end{definition}

\begin{definition}\label{follower_index}
    $y$ follows $x$ in $I$ iff $x < y$ and $x,y \in I$ and for all $i \in I$ such that $x < i$ we have $y \leq i$.
\end{definition}

\begin{definition}\label{finer_smallest_step}
    $Y$ is a minimal finer extention of $X$ in $U$ iff $Y$ is finer then $X$ in $U$ and for all $x_1,x_2 \in \dom{X}$ such that $x_1$ follows $x_2$ in $\dom{X}$ we have there exist $y \in \dom{Y}$ such that $y$ follows $x_1$ in $\dom{X}$ and $x_2$ follows $y$ in $\dom{X}$.
\end{definition}

\begin{definition}\label{sequence_of_reals}
    $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$.
\end{definition}


\begin{definition}\label{pointwise_convergence}
    $X$ converge to $x$ iff for all $\epsilon \in \realsplus$ there exist $N \in \dom{X}$ such that for all $n \in \dom{X}$ such that $n > N$ we have $\at{X}{n} \in \epsBall{x}{\epsilon}$.
\end{definition}


\begin{proposition}\label{iff_sequence}
    Suppose $X$ is a function.
    Suppose $\dom{X} \subseteq \naturals$.
    Then $X$ is a sequence.
\end{proposition}

\begin{definition}\label{lifted_urysohn_chain}
    $U$ is a lifted urysohnchain of $X$ iff $U$ is a sequence and $\dom{U} = \naturals$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
\end{definition}

\begin{definition}\label{normal_ordered_urysohnchain}
    $U$ is normal ordered iff there exist $n \in \naturals$ such that $\dom{U} = \seq{\zero}{n}$.
\end{definition}

\begin{definition}\label{bijection_of_urysohnchains}
    $f$ is consistent on $X$ to $Y$ iff $f$ is a bijection from $\dom{X}$ to $\dom{Y}$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $f(n) < f(m)$.
\end{definition}

\begin{proposition}\label{naturals_in_transitive}
    $\naturals$ is a \in-transitive set.
\end{proposition}

\begin{proposition}\label{naturals_elem_in_transitive}
    If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
    %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
\end{proposition}

\begin{proposition}\label{natural_number_is_ordinal_for_all}
    For all $n \in \naturals$ we have $n$ is a ordinal.
\end{proposition}

\begin{proposition}\label{zero_is_in_minimal}
    $\zero$ is an \in-minimal element of $\naturals$.
\end{proposition}

\begin{proposition}\label{natural_rless_eq_precedes}
    For all $n,m \in \naturals$ we have $n \precedes m$ iff $n \in m$.
\end{proposition}

\begin{proposition}\label{naturals_precedes_suc}
    For all $n \in \naturals$ we have $n \precedes \suc{n}$.
\end{proposition}

\begin{proposition}\label{zero_is_empty}
    There exists no $x$ such that $x \in \zero$.
\end{proposition}

\begin{proposition}\label{one_is_positiv}
    $1$ is positiv.
\end{proposition}

\begin{proposition}\label{suc_of_positive_is_positive}
    For all $n \in \naturals$ such that $n$ is positiv we have $\suc{n}$ is positiv.
\end{proposition}

\begin{proposition}\label{naturals_are_positiv_besides_zero}
    For all $n \in \naturals$ such that $n \neq \zero$ we have $n$ is positiv.
\end{proposition}
\begin{proof}[Proof by \in-induction on $n$]
    Assume $n \in \naturals$.
    \begin{byCase}
        \caseOf{$n = \zero$.} Trivial.
        \caseOf{$n \neq \zero$.}
            Take $k \in \naturals$ such that $\suc{k} = n$.
    \end{byCase}
\end{proof}



\begin{proposition}\label{naturals_sum_eq_zero}
    For all $n,m \in \naturals$ we have if $n+m = \zero$ then $n = m = \zero$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{no_natural_between_n_and_suc_n}
    For all $n,m \in \naturals$ we have not $n < m < \suc{n}$.
\end{proposition}

\begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
    For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
\end{proposition}
\begin{proof}[Proof by \in-induction on $n$]
    Assume $n \in \naturals$.
    We show that $\naturals = (\{\zero, 1\} \union \{n \in \naturals \mid n > 1\})$.
    \begin{subproof}
        Trivial.
    \end{subproof}
    \begin{byCase}
        \caseOf{$n = \zero$.} 
            
            We show that for all $m \in \naturals$ such that $m < n$ we have there exist $k \in \naturals$ such that $m + k = n$.
            \begin{subproof}[Proof by \in-induction on $m$]
                Assume $m \in \naturals$.
                \begin{byCase}
                    \caseOf{$m = \zero$.}
                        Trivial.
                    \caseOf{$m \neq \zero$.}
                        Trivial.
                \end{byCase}
            \end{subproof}
        \caseOf{$n = 1$.}
            Fix $m$.
            For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$.
            Then $\zero + 1 = 1$.
        \caseOf{$n > 1$.} 
            Take $l \in \naturals$ such that $\suc{l} = n$.
            Omitted.
    \end{byCase}
\end{proof}


\begin{proposition}\label{rless_eq_in_for_naturals}
    For all $n,m \in \naturals$ such that $n < m$ we have $n \in m$. 
\end{proposition}
\begin{proof}
    We show that for all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ we have $m \in n$.
    \begin{subproof}[Proof by \in-induction on $n$]
        Assume $n \in \naturals$.
        We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$.
        \begin{subproof}[Proof by \in-induction on $m$]
            Assume $m \in \naturals$.
            %\begin{byCase}
            %    
            %\end{byCase}
        \end{subproof}
    \end{subproof}
    
    %Fix $n \in \naturals$.

    %\begin{byCase}
    %    \caseOf{$n = \zero$.}
    %        For all $k \in \naturals$ we have $k = \zero$ or $\zero < k$.
    %        
    %    \caseOf{$n \neq \zero$.}
    %        Fix $m \in \naturals$.
    %        It suffices to show that $m \in n$.
    %\end{byCase}
    
\end{proof}



\begin{proposition}\label{naturals_leq}
    For all $n \in \naturals$ we have $\zero \leq n$.
\end{proposition}



\begin{proposition}\label{naturals_leq_on_suc}
    For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$.
\end{proposition}
\begin{proof}
    Omitted.
\end{proof}

\begin{proposition}\label{x_in_seq_iff}
    Suppose $n,m,x \in \naturals$.
    $x \in \seq{n}{m}$ iff $n \leq x \leq m$.
\end{proposition}

\begin{proposition}\label{seq_zero_to_n_eq_to_suc_n}
    For all $n \in \naturals$ we have $\seq{\zero}{n} = \suc{n}$.
\end{proposition}
\begin{proof} [Proof by \in-induction on $n$]
    Assume $n \in \naturals$.
    $n \in \naturals$.
    For all $m \in n$ we have $m \in \naturals$.
    \begin{byCase}
        \caseOf{$n = \zero$.}
            It suffices to show that $1 = \seq{\zero}{\zero}$.
            Follows by set extensionality.
        \caseOf{$n \neq \zero$.}
            Take $k$ such that $k \in \naturals$ and $\suc{k} = n$.
            Then $k \in n$.
            Therefore $\seq{\zero}{k} = \suc{k}$.
            We show that $\seq{\zero}{n} = \seq{\zero}{k} \union \{n\}$.
            \begin{subproof}
                We show that $\seq{\zero}{n} \subseteq \seq{\zero}{k} \union \{n\}$.
                \begin{subproof}
                    It suffices to show that for all $x \in \seq{\zero}{n}$ we have $x \in \seq{\zero}{k} \union \{n\}$.
                    $n \in \naturals$.
                    $\zero \leq n$.
                    $n \leq n$.
                    We have $n \in \seq{\zero}{n}$.
                    Therefore $\seq{\zero}{n}$ is inhabited.
                    Take $x$ such that $x \in \seq{\zero}{n}$.
                    Therefore $\zero \leq x \leq n$.
                    $x = n$ or $x < n$.
                    Then either $x = n$ or $x \leq k$.
                    Therefore $x \in \seq{\zero}{k}$ or $x = n$.
                    Follows by \cref{reals_order,natural_number_is_ordinal,ordinal_empty_or_emptyset_elem,naturals_leq_on_suc,reals_axiom_zero_in_reals,naturals_subseteq_reals,subseteq,union_intro_left,naturals_inductive_set,m_to_n_set,x_in_seq_iff,union_intro_right,singleton_intro}.
                \end{subproof}
                We show that $\seq{\zero}{k} \union \{n\} \subseteq \seq{\zero}{n}$.
                \begin{subproof}
                    It suffices to show that for all $x \in \seq{\zero}{k} \union \{n\}$ we have $x \in \seq{\zero}{n}$.
                    $k \leq n$ by \cref{naturals_subseteq_reals,suc_eq_plus_one,plus_one_order,subseteq}.
                    $k \in n$.
                    $\seq{\zero}{k} = \suc{k}$ by assumption.            
                    $n \in \naturals$.
                    $\zero \leq n$.
                    $n \leq n$.
                    We have $n \in \seq{\zero}{n}$.
                    Therefore $\seq{\zero}{n}$ is inhabited.
                    Take $x$ such that $x \in \seq{\zero}{n}$.
                    Therefore $\zero \leq x \leq n$.
                    $x = n$ or $x < n$.
                    Then either $x = n$ or $x \leq k$.
                    Therefore $x \in \seq{\zero}{k}$ or $x = n$.
                    Fix $x$.
                    \begin{byCase}
                        \caseOf{$x \in \seq{\zero}{k}$.}
                            Trivial.
                        \caseOf{$x = n$.}
                            It suffices to show that $n \in \seq{\zero}{n}$.
                    \end{byCase}
                \end{subproof}
                Trivial.
            \end{subproof}
            We have $\suc{n} = n \union \{n\}$.
    \end{byCase}

    %Assume $n$ is a natural number.
    %We show that $\seq{\zero}{\zero}$ has cardinality $1$.
    %\begin{subproof}
    %    It suffices to show that $1 = \seq{\zero}{\zero}$.
    %    Follows by set extensionality.
    %\end{subproof}
    %It suffices to show that if $n \neq \zero$ then $\seq{\zero}{n}$ has cardinality $\suc{n}$.
    %We show that for all $m \in \naturals$ such that $m \neq \zero$ we have $\seq{\zero}{m}$ has cardinality $\suc{m}$.
    %\begin{subproof}
    %    Fix $m \in \naturals$.
    %    Take $k$ such that $k \in \naturals$ and $\suc{k} = m$.
    %    Then $k \in m$.
    %\end{subproof}
    
    
    %For all $n \in \naturals$ we have either $n = \zero$ or there exist $m \in \naturals$ such that $n = \suc{m}$.
    %For all $n \in \naturals$ we have either $n = \zero$ or $\zero \in n$.
    %We show that if $\seq{\zero}{n}$ has cardinality $\suc{n}$ then $\seq{\zero}{\suc{n}}$ has cardinality $\suc{\suc{n}}$.
    %\begin{subproof}
    %    Omitted.
    %\end{subproof}
\end{proof}

\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
\end{proposition}

\begin{proposition}\label{existence_normal_ordered_urysohn}
    Let $X$ be a urysohn space.
    Suppose $U$ is a urysohnchain of $X$.
    Suppose $\dom{U}$ is finite.
    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $X$ to $Y$ and $V$ is normal ordered.
\end{proposition}
\begin{proof}
    Take $k$ such that $\dom{U}$ has cardinality $k$ by \cref{ran_converse,cardinality,finite}.
    There exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$.


\end{proof}


\begin{definition}\label{staircase}
    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$.
\end{definition}

\begin{definition}\label{staircase_sequence}
    $f$ is staircase sequence of $U$ iff $f$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{f}$ and for all $n \in \dom{U}$ we have $\at{f}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
\end{definition}





\begin{theorem}\label{urysohnsetinbeetween}
    Let $X$ be a urysohn space.
    Suppose $A,B \in \closeds{X}$.
    Suppose $\closure{A}{X} \subseteq \interior{B}{X}$.
    Suppose $\carrier[X]$ is inhabited.
    There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$.
\end{theorem}
\begin{proof}
    Omitted.
\end{proof}


\begin{theorem}\label{induction_on_urysohnchains}
    Let $X$ be a urysohn space.
    Suppose $U_0$ is a sequence.
    Suppose $U_0$ is a chain of subsets in $X$.
    Suppose $U_0$ is a urysohnchain of $X$.
    There exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
\end{theorem}
\begin{proof}
    %$U_0$ is a urysohnchain of $X$.
    %It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
    Omitted.
\end{proof}





\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}
    Let $X' = \carrier[X]$.
    Let $N = \{\zero, 1\}$.
    $1 = \suc{\zero}$.
    $1 \in \naturals$ and $\zero \in \naturals$.
    $N \subseteq \naturals$.
    Let $A' = (X' \setminus B)$.
    $B \subseteq X'$ by \cref{powerset_elim,closeds}.
    $A \subseteq X'$.
    Therefore $A \subseteq A'$.
    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =$
    \begin{cases}
        &A  &\text{if} n = \zero \\
        &A' &\text{if} n = 1
    \end{cases}
    $U_0$ is a function.
    $\dom{U_0} = N$.
    $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
    $U_0$ is a sequence.
    We have $1, \zero \in N$.
    We show that $U_0$ is a chain of subsets in $X$.
    \begin{subproof}
        We have $\dom{U_0} \subseteq \naturals$.
        We have for all $n \in \dom{U_0}$ we have $\at{U_0}{n} \subseteq \carrier[X]$ by \cref{topological_prebasis_iff_covering_family,union_as_unions,union_absorb_subseteq_left,subset_transitive,setminus_subseteq}.
        We have $\dom{U_0} = \{\zero, 1\}$.

        It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $m > n$ we have $\at{U_0}{n} \subseteq \at{U_0}{m}$.

        Fix $n \in \dom{U_0}$.
        Fix $m \in \dom{U_0}$.

        \begin{byCase}
            \caseOf{$n \neq \zero$.} 
                Trivial.
            \caseOf{$n = \zero$.} 
                \begin{byCase}
                    \caseOf{$m = \zero$.} 
                        Trivial.
                    \caseOf{$m \neq \zero$.}
                        We have $A \subseteq A'$.
                        We have $\at{U_0}{\zero} = A$ by assumption.
                        We have $\at{U_0}{1}= A'$ by assumption.
                        Follows by \cref{powerset_elim,emptyset_subseteq,union_as_unions,union_absorb_subseteq_left,subseteq_pow_unions,ran_converse,subseteq,subseteq_antisymmetric,suc_subseteq_intro,apply,powerset_emptyset,emptyset_is_ordinal,notin_emptyset,ordinal_elem_connex,omega_is_an_ordinal,prec_is_ordinal}.
                \end{byCase}
        \end{byCase}
    \end{subproof}

    We show that $U_0$ is a urysohnchain of $X$.
    \begin{subproof}
        It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $n < m$ we have $\closure{\at{U_0}{n}}{X} \subseteq \interior{\at{U_0}{m}}{X}$.
        Fix $n \in \dom{U_0}$.
        Fix $m \in \dom{U_0}$.
        \begin{byCase}
            \caseOf{$n \neq \zero$.} 
                Follows by \cref{ran_converse,upair_iff,one_in_reals,order_reals_lemma0,reals_axiom_zero_in_reals,reals_one_bigger_zero,reals_order}.
            \caseOf{$n = \zero$.} 
                \begin{byCase}
                    \caseOf{$m = \zero$.} 
                        Trivial.
                    \caseOf{$m \neq \zero$.}
                        Follows by \cref{setminus_emptyset,setdifference_eq_intersection_with_complement,setminus_self,interior_carrier,complement_interior_eq_closure_complement,subseteq_refl,closure_interior_frontier_is_in_carrier,emptyset_subseteq,closure_is_minimal_closed_set,inter_lower_right,inter_lower_left,subseteq_transitive,interior_of_open,is_closed_in,closeds,union_absorb_subseteq_right,ordinal_suc_subseteq,ordinal_empty_or_emptyset_elem,union_absorb_subseteq_left,union_emptyset,topological_prebasis_iff_covering_family,inhabited,notin_emptyset,subseteq,union_as_unions,natural_number_is_ordinal}.
                \end{byCase}
        \end{byCase}
    \end{subproof}
    %We are done with the first step, now we want to prove that we have U a sequence of these chain with U_0 the first chain.

    We show that there exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
    \begin{subproof}
        Follows by \cref{chain_of_subsets,urysohnchain,induction_on_urysohnchains}.
    \end{subproof}
    Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.





    
\end{proof}

\begin{theorem}\label{safe}
    Contradiction.     
\end{theorem}





%
%Ideen:
%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat
%
%zulässig und verfeinerung von ketten als predicat definieren. 
%
%limits und punkt konvergenz als prädikat.
%
%
%Vor dem Beweis vor dem eigentlichen Beweis.
%die abgeleiteten Funktionen
%
%\derivedstiarcasefunction on A
%
%abbreviation: \at{f}{n} = f_{n}
%
%
%TODO:
%Reals ist ein topologischer Raum
%