From f45b3278abcf30ee12fdbb43a579412ba0da7d8d Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Fri, 4 Jul 2025 02:03:57 +0200 Subject: Rename for compat --- library/topology/urysohn2.tex | 989 ---------------------------------------- library/topology/urysohntwo.tex | 989 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 989 insertions(+), 989 deletions(-) delete mode 100644 library/topology/urysohn2.tex create mode 100644 library/topology/urysohntwo.tex (limited to 'library') diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex deleted file mode 100644 index a1a3ba0..0000000 --- a/library/topology/urysohn2.tex +++ /dev/null @@ -1,989 +0,0 @@ -\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} -\import{set/equinumerosity.tex} - -\section{Urysohns Lemma}\label{form_sec_urysohn} - - - - -\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 $n < m$ 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 $B$ to $C$ in $X$ iff $\closure{B}{X} \subseteq \interior{A}{X}$ and $\closure{A}{X} \subseteq \interior{C}{X}$. -\end{definition} - -\begin{definition}\label{finer} %<-- verfeinerung - $A$ is finer then $B$ in $X$ iff for all $n \in \dom{B}$ we have $\at{B}{n} \in \ran{A}$ and for all $m \in \dom{B}$ such that $n < m$ we have there exist $k \in \dom{A}$ such that $\at{A}{k}$ is finer between $\at{B}{n}$ to $\at{B}{m}$ in $X$. -\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{definition}\label{staircase} -% $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and there exist $k \in \naturals$ such that $k = \max{\dom{U}}$ and for all $x,y \in \carrier[X]$ such that $y \in \carrier[X] \setminus \at{U}{k}$ and $x \in \at{U}{k}$ we have $f(y) = 1$ and there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ and $f(x)= \rfrac{m}{k}$. -%\end{definition} - - -\begin{definition}\label{staircase_step_value1} - $a$ is the staircase step value at $y$ of $U$ in $X$ iff there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $y \in \closure{\at{U}{n}}{X} \setminus \closure{\at{U}{m}}{X}$ and $a = \rfrac{n}{\max{\dom{U}}}$. -\end{definition} - -\begin{definition}\label{staircase_step_value2} - $a$ is the staircase step valuetwo at $y$ of $U$ in $X$ iff either if $y \in (\carrier[X] \setminus \closure{\at{U}{\max{\dom{U}}}}{X})$ then $a = 1$ or $a$ is the staircase step valuethree at $y$ of $U$ in $X$. -\end{definition} - -\begin{definition}\label{staircase_step_value3} - $a$ is the staircase step valuethree at $y$ of $U$ in $X$ iff if $y \in \closure{\at{U}{\min{\dom{U}}}}{X}$ then $f(z) = \zero$. -\end{definition} - - -\begin{definition}\label{staircase2} - $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and for all $y \in \carrier[X]$ we have either $f(y)$ is the staircase step value at $y$ of $U$ in $X$ or $f(y)$ is the staircase step valuetwo at $y$ of $U$ in $X$. -\end{definition} - -\begin{definition}\label{staircase_sequence} - $S$ is staircase sequence of $U$ in $X$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. -\end{definition} - -\begin{definition}\label{staircase_limit_point} - $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$. -\end{definition} - -%\begin{definition}\label{staircase_limit_function} -% $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$. -%\end{definition} -% -\begin{definition}\label{staircase_limit_function} - $f$ is the limit function of staircase $S$ together with $U$ and $X$ iff $S$ is staircase sequence of $U$ in $X$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$. -\end{definition} - - -\begin{proposition}\label{naturals_in_transitive} - $\naturals$ is a \in-transitive set. -\end{proposition} -\begin{proof} - Follows by \cref{nat_is_transitiveset}. -\end{proof} - -\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{proof} - Follows by \cref{notin_emptyset}. -\end{proof} - -\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{proof} - Omitted. -\end{proof} - -\begin{proposition}\label{naturals_is_zero_one_or_greater} - $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$. -\end{proposition} -\begin{proof} - Omitted. -\end{proof} - -\begin{proposition}\label{naturals_one_zero_or_greater} - For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$. -\end{proposition} -\begin{proof} - Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}. -\end{proof} - -\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$. - - \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} - \caseOf{$\suc{m}=n$.} - \caseOf{$\suc{m}\neq n$.} - \begin{byCase} - \caseOf{$n = \zero$.} - \caseOf{$n \neq \zero$.} - Take $l \in \naturals$ such that $\suc{l} = n$. - Omitted. - - \end{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{bijection_naturals_order} - For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. -\end{proposition} -\begin{proof} - Omitted. -\end{proof} - -\begin{lemma}\label{naturals_suc_injective} - Suppose $n,m \in \naturals$. - $n = m$ iff $\suc{n} = \suc{m}$. -\end{lemma} - -\begin{lemma}\label{naturals_rless_implies_not_eq} - Suppose $n,m \in \naturals$. - Suppose $n < m$. - Then $n \neq m$. -\end{lemma} - -\begin{lemma}\label{cardinality_of_singleton} - For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$. -\end{lemma} -\begin{proof} - Omitted. - %Fix $x$. - %Suppose $x \neq \emptyset$. - %Let $X = \{x\}$. - %$\seq{\zero}{\zero}=1$. - %$\seq{\zero}{\zero}$ has cardinality $1$. - %$X \setminus \{x\} = \emptyset$. - %$1 = \{\emptyset\}$. - %Let $F = \{(x,\emptyset)\}$. - %$F$ is a relation. - %$\dom{F} = X$. - %$\emptyset \in \ran{F}$. - %for all $x \in 1$ we have $x = \emptyset$. - %$\ran{F} = 1$. - %$F$ is injective. - %$F \in \surj{X}{1}$. - %$F$ is a bijection from $X$ to $1$. -\end{proof} - -\begin{lemma}\label{cardinality_n_plus_1} - For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$. -\end{lemma} -\begin{proof} - Omitted. -\end{proof} - -\begin{lemma}\label{cardinality_n_m_plus} - For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$. -\end{lemma} -\begin{proof} - Omitted. -\end{proof} - -\begin{lemma}\label{cardinality_plus_disjoint} - Suppose $X \inter Y = \emptyset$. - Suppose $X$ is finite. - Suppose $Y$ is finite. - Suppose $X$ has cardinality $n$. - Suppose $Y$ has cardinality $m$. - Then $X \union Y$ has cardinality $m+n$. -\end{lemma} -\begin{proof} - Omitted. -\end{proof} - - - - -\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1} - Suppose $f$ is a bijection from $X$ to $Y$. - Suppose $g$ is a function from $X$ to $Y$. - Suppose $g$ is injective. - Suppose $X$ is finite and $Y$ is finite. - For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$. -\end{lemma} -\begin{proof}[Proof by \in-induction on $n$] - Assume $n \in \naturals$. - Suppose $Y$ has cardinality $n$. - $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}. - \begin{byCase} - \caseOf{$n = \zero$.} - Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}. - \caseOf{$n \neq \zero$.} - %Take $n' \in n$ such that $n = \suc{n'}$. - %$n' \in \naturals$. - %$n' + 1 = n$. - %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. - %Let $Y' = Y \setminus \{y\}$. - %$Y' \subseteq Y$. - %$Y'$ is finite. - %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$. - %Take $m \in \naturals$ such that $Y'$ has cardinality $m$. - %Then $Y'$ has cardinality $n'$. - %Let $x' = \apply{\converse{f}}{y'}$. - %$x' \in X$. - %Let $X' = X \setminus \{x'\}$. - %$X' \subseteq X$. - %$X'$ is finite. - %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$. - %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$. - %Then $X'$ has cardinality $n'$. - %Let $f'(z)=f(z)$ for $z \in X'$. - %$\dom{f'} = X'$. - %$\ran{f'} = Y'$. - %$f'$ is a bijection from $X'$ to $Y'$. - %Let $g'(z) = g(z)$ for $z \in X'$. - %Then $g'$ is injective. - %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}. - %Define $G : X \to Y$ such that $G(z)= - %\begin{cases} - % g'(z) & \text{if} z \in X' \\ - % y' & \text{if} z = x' - %\end{cases}$ - %$G = g$. - %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}. - Omitted. - \end{byCase} - %$\converse{f}$ is a bijection from $Y$ to $X$. - %Let $h = g \circ \converse{f}$. - %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}. - %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}. -% - %Fix $y \in Y$. - %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$. - -\end{proof} - -\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection} - Suppose $f$ is a bijection from $X$ to $Y$. - Suppose $g$ is a function from $X$ to $Y$. - Suppose $g$ is injective. - Suppose $Y$ is finite. - Then $g$ is a bijection from $X$ to $Y$. -\end{lemma} -\begin{proof} - There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}. - Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}. -\end{proof} - - - -\begin{lemma}\label{naturals_bijection_implies_eq} - Suppose $n,m \in \naturals$. - Suppose $f$ is a bijection from $n$ to $m$. - Then $n = m$. -\end{lemma} -\begin{proof} - $n$ is finite. - $m$ is finite. - Suppose not. - Then $n < m$ or $m < n$. - \begin{byCase} - \caseOf{$n < m$.} - Then $n \in m$. - There exist $x \in m$ such that $x \notin n$. - $\identity{n}$ is a function from $n$ to $m$. - $\identity{n}$ is injective. - $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. - Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. - \caseOf{$m < n$.} - Then $m \in n$. - There exist $x \in n$ such that $x \notin m$. - $\converse{f}$ is a bijection from $m$ to $n$. - $\identity{m}$ is a function from $m$ to $n$. - $\identity{m}$ is injective. - $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. - Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. - \end{byCase} -\end{proof} - -\begin{lemma}\label{naturals_eq_iff_bijection} - Suppose $n,m \in \naturals$. - $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$. -\end{lemma} -\begin{proof} - We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$. - \begin{subproof} - Trivial. - \end{subproof} - We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$. - \begin{subproof}%[Proof by \in-induction on $k$] - %Assume $k \in \naturals$. - %\begin{byCase} - % \caseOf{$k = \zero$.} - % Trivial. - % \caseOf{$k \neq \zero$.} - % \begin{byCase} - % \caseOf{$m = \zero$.} - % Trivial. - % \caseOf{$m \neq \zero$.} - % Take $k' \in \naturals$ such that $\suc{k'} = k$. - % Then $k' \in k$. - % Take $m' \in \naturals$ such that $m = \suc{m'}$. - % Then $m' \in m$. - % - % \end{byCase} - %\end{byCase} - \end{subproof} -\end{proof} - -\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border} - Suppose $n,m \in \naturals$. - Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. - Then $n = m$. -\end{lemma} -\begin{proof} - We have $\seq{\zero}{n} = \suc{n}$. - Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$. - Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}. -\end{proof} - -\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq} - Suppose $n,m \in \naturals$. - Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. - Then $\seq{\zero}{n} = \seq{\zero}{m}$. -\end{lemma} - -\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. - Suppose $U$ is inhabited. - Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered. -\end{proposition} -\begin{proof} - Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}. - \begin{byCase} - \caseOf{$n = \zero$.} - Omitted. - \caseOf{$n \neq \zero$.} - Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. - We have $\dom{U} \subseteq \naturals$. - $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}. - $\dom{U}$ has cardinality $\suc{k}$. - We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. - \begin{subproof} - For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. - We have $\dom{U} \subseteq \naturals$. - $\dom{U}$ is inhabited. - Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. - Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. - Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. - $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}. - $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}. - %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$. - %\begin{subproof} - % We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$. - % \begin{subproof} - % It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$. - % Fix $y \in \seq{\emptyset}{k'}$. - % Then $y \leq k'$. - % Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}. - % - % Therefore $y \in \suc{k}$. - % Therefore $y \in \seq{\emptyset}{k}$. - % \end{subproof} - % We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$. - % \begin{subproof} - % Fix $y \in \seq{\emptyset}{k}$. - % \end{subproof} - %\end{subproof} - \end{subproof} - Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. - Let $N = \seq{\zero}{k}$. - Let $M = \pow{X}$. - Define $V : N \to M$ such that $V(n)= - \begin{cases} - \at{U}{F(n)} & \text{if} n \in N - \end{cases}$ - $\dom{V} = \seq{\zero}{k}$. - We show that $V$ is a urysohnchain of $X$. - \begin{subproof} - It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$. - We show that $V$ is a chain of subsets in $X$. - \begin{subproof} - It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$. - $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}. - It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$. - Fix $n \in \dom{V}$. - Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. - It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$. - Fix $m$ such that $m \in \dom{V}$ and $n \rless m$. - Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. - \end{subproof} - It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$. - Fix $n \in \dom{V}$. - Fix $m$ such that $m \in \dom{V} \land n \rless m$. - Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. - \end{subproof} - We show that $F$ is consistent on $V$ to $U$. - \begin{subproof} - It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}. - $F$ is a bijection from $\dom{V}$ to $\dom{U}$. - It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$. - Fix $n \in \dom{V}$. - Fix $m$ such that $m \in \dom{V}$ and $n \rless m$. - Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. - \end{subproof} - $V$ is normal ordered. - \end{byCase} - -\end{proof} - - -\begin{proposition}\label{staircase_ran_in_zero_to_one} - Let $X$ be a urysohn space. - Suppose $U$ is a urysohnchain of $X$. - Suppose $f$ is a staircase function adapted to $U$ in $X$. - Then $\ran{f} \subseteq \intervalclosed{\zero}{1}$. -\end{proposition} -\begin{proof} - Omitted. -\end{proof} - -\begin{proposition}\label{staircase_limit_is_continuous} - Let $X$ be a urysohn space. - Suppose $U$ is a lifted urysohnchain of $X$. - Suppose $S$ is staircase sequence of $U$ in $X$. - Suppose $f$ is the limit function of staircase $S$ together with $U$ and $X$. - Then $f$ is continuous. -\end{proposition} -\begin{proof} - Omitted. -\end{proof} - -\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{lemma}\label{fractions_between_zero_one} - Suppose $n,m \in \naturals$. - Suppose $m > n$. - Then $\zero \leq \rfrac{n}{m} \leq 1$. -\end{lemma} -\begin{proof} - Omitted. -\end{proof} - -\begin{lemma}\label{intervalclosed_border_is_elem} - Suppose $a,b \in \reals$. - Suppose $a < b$. - Then $a,b \in \intervalclosed{a}{b}$. -\end{lemma} - -\begin{lemma}\label{urysohnchain_subseteqrel} - Let $X$ be a urysohn space. - Suppose $U$ is a urysohnchain of $X$. - Then for all $n,m \in \dom{U}$ such that $n < m$ we have $\at{U}{n} \subseteq \at{U}{m}$. -\end{lemma} - - -\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$ is continuous - and for all $a,b$ such that $a \in A$ and $b \in B$ we have $f(a)= \zero$ and $f(b) = 1$. -\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$. - - We show that there exist $S$ such that $S$ is staircase sequence of $U$ in $X$. - \begin{subproof} - Omitted. - \end{subproof} - Take $S$ such that $S$ is staircase sequence of $U$ in $X$. - - %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$. -% - %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for . - We show that there exist $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$. - \begin{subproof} - Omitted. - \end{subproof} - Take $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$. - Then $f$ is continuous. - We show that $\dom{f} = \carrier[X]$. - \begin{subproof} - Trivial. - \end{subproof} - $f$ is a function. - We show that $\ran{f} \subseteq \intervalclosed{\zero}{1}$. - \begin{subproof} - It suffices to show that $f$ is a function to $\intervalclosed{\zero}{1}$. - It suffices to show that for all $x \in \dom{f}$ we have $f(x) \in \intervalclosed{\zero}{1}$. - Fix $x \in \dom{f}$. - $f(x)$ is the staircase limit of $S$ with $x$. - Therefore $f(x) \in \reals$. - - We show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. - \begin{subproof} - Fix $n \in \naturals$. - Let $g = \at{S}{n}$. - Let $U' = \at{U}{n}$. - $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. - $g$ is a staircase function adapted to $U'$ in $X$. - $U'$ is a urysohnchain of $X$. - $g$ is a function from $\carrier[X]$ to $\reals$. - It suffices to show that $\ran{g} \subseteq \intervalclosed{\zero}{1}$ by \cref{function_apply_default,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,function_apply_elim,inter,inter_absorb_supseteq_left,ran_iff,funs_is_relation,funs_is_function,staircase2}. - 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]$. - \begin{byCase} - \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.} - Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$. - We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$. - \begin{subproof} - Omitted. - \end{subproof} - Therefore $x \notin (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$. - We show that $g(x) = 1$. - \begin{subproof} - Omitted. - \end{subproof} - \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.} - \begin{byCase} - \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.} - We show that $g(x) = \zero$. - \begin{subproof} - Omitted. - \end{subproof} - \caseOf{$x \in (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.} - Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$. - Omitted. - \end{byCase} - \end{byCase} - - - - %$\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. - %$\at{U}{n}$ is a urysohnchain of $X$. - %$\at{S}{n}$ is a function from $\carrier[X]$ to $\reals$. - %there exist $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$. - %Take $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$. - %\begin{byCase} - % \caseOf{$x \in \carrier[X] \setminus \at{\at{U}{n}}{k}$.} - % $1 \in \intervalclosed{\zero}{1}$. - % We show that for all $y \in (\carrier[X] \setminus \at{\at{U}{n}}{k})$ we have $\apply{\at{S}{n}}{y} = 1$. - % \begin{subproof} - % Omitted. - % \end{subproof} - % Then $\apply{\at{S}{n}}{x} = 1$. - % \caseOf{$x \notin \carrier[X] \setminus \at{\at{U}{n}}{k}$.} - % %There exist $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$. - % Take $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$. - % Then $\apply{\at{S}{n}}{x} = \rfrac{m'}{k'}$. - % It suffices to show that $\rfrac{m'}{k'} \in \intervalclosed{\zero}{1}$. - % $\zero \leq m' \leq k$. - %\end{byCase} - %%It suffices to show that $\zero \leq \apply{\at{S}{n}}{x} \leq 1$. - %%It suffices to show that $\ran{\at{S}{n}} \subseteq \intervalclosed{\zero}{1}$. - \end{subproof} - - Suppose not. - Then $f(x) < \zero$ or $f(x) > 1$ by \cref{reals_order_total,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,one_in_reals}. - For all $\epsilon \in \realsplus$ we have there exist $m \in \naturals$ such that $\apply{\at{S}{m}}{x} \in \epsBall{f(x)}{\epsilon}$ by \cref{plus_one_order,naturals_is_equal_to_two_times_naturals,subseteq,naturals_subseteq_reals,staircase_limit_point}. - \begin{byCase} - \caseOf{$f(x) < \zero$.} - Let $\delta = \zero - f(x)$. - $\delta \in \realsplus$. - It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$. - Fix $n \in \naturals$. - $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. - For all $y \in \epsBall{f(x)}{\delta}$ we have $y < \zero$ by \cref{epsilon_ball,minus_behavior1,minus_behavior3,minus,apply,intervalopen}. - It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. - Trivial. - \caseOf{$f(x) > 1$.} - Let $\delta = f(x) - 1$. - $\delta \in \realsplus$. - It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$. - Fix $n \in \naturals$. - $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. - For all $y \in \epsBall{f(x)}{\delta}$ we have $y > 1$ by \cref{epsilon_ball,reals_addition_minus_behavior2,minus_in_reals,apply,reals_addition_minus_behavior1,minus,reals_add,realsplus_in_reals,one_in_reals,reals_axiom_kommu,intervalopen}. - It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. - Trivial. - \end{byCase} - - \end{subproof} - Therefore $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ by \cref{staircase_limit_function,surj_to_fun,fun_to_surj,neq_witness,inters_of_ordinals_elem,times_tuple_elim,img_singleton_iff,foundation,subseteq_emptyset_iff,inter_eq_left_implies_subseteq,inter_emptyset,funs_intro,fun_ran_iff,not_in_subseteq}. - - We show that for all $a \in A$ we have $f(a) = \zero$. - \begin{subproof} - Omitted. - \end{subproof} - We show that for all $b \in B$ we have $f(b) = 1$. - \begin{subproof} - Omitted. - \end{subproof} - - -\end{proof} - -%\begin{theorem}\label{safe} -% Contradiction. -%\end{theorem} - - - - - - diff --git a/library/topology/urysohntwo.tex b/library/topology/urysohntwo.tex new file mode 100644 index 0000000..a1a3ba0 --- /dev/null +++ b/library/topology/urysohntwo.tex @@ -0,0 +1,989 @@ +\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} +\import{set/equinumerosity.tex} + +\section{Urysohns Lemma}\label{form_sec_urysohn} + + + + +\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 $n < m$ 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 $B$ to $C$ in $X$ iff $\closure{B}{X} \subseteq \interior{A}{X}$ and $\closure{A}{X} \subseteq \interior{C}{X}$. +\end{definition} + +\begin{definition}\label{finer} %<-- verfeinerung + $A$ is finer then $B$ in $X$ iff for all $n \in \dom{B}$ we have $\at{B}{n} \in \ran{A}$ and for all $m \in \dom{B}$ such that $n < m$ we have there exist $k \in \dom{A}$ such that $\at{A}{k}$ is finer between $\at{B}{n}$ to $\at{B}{m}$ in $X$. +\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{definition}\label{staircase} +% $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and there exist $k \in \naturals$ such that $k = \max{\dom{U}}$ and for all $x,y \in \carrier[X]$ such that $y \in \carrier[X] \setminus \at{U}{k}$ and $x \in \at{U}{k}$ we have $f(y) = 1$ and there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ and $f(x)= \rfrac{m}{k}$. +%\end{definition} + + +\begin{definition}\label{staircase_step_value1} + $a$ is the staircase step value at $y$ of $U$ in $X$ iff there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $y \in \closure{\at{U}{n}}{X} \setminus \closure{\at{U}{m}}{X}$ and $a = \rfrac{n}{\max{\dom{U}}}$. +\end{definition} + +\begin{definition}\label{staircase_step_value2} + $a$ is the staircase step valuetwo at $y$ of $U$ in $X$ iff either if $y \in (\carrier[X] \setminus \closure{\at{U}{\max{\dom{U}}}}{X})$ then $a = 1$ or $a$ is the staircase step valuethree at $y$ of $U$ in $X$. +\end{definition} + +\begin{definition}\label{staircase_step_value3} + $a$ is the staircase step valuethree at $y$ of $U$ in $X$ iff if $y \in \closure{\at{U}{\min{\dom{U}}}}{X}$ then $f(z) = \zero$. +\end{definition} + + +\begin{definition}\label{staircase2} + $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and for all $y \in \carrier[X]$ we have either $f(y)$ is the staircase step value at $y$ of $U$ in $X$ or $f(y)$ is the staircase step valuetwo at $y$ of $U$ in $X$. +\end{definition} + +\begin{definition}\label{staircase_sequence} + $S$ is staircase sequence of $U$ in $X$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. +\end{definition} + +\begin{definition}\label{staircase_limit_point} + $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$. +\end{definition} + +%\begin{definition}\label{staircase_limit_function} +% $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$. +%\end{definition} +% +\begin{definition}\label{staircase_limit_function} + $f$ is the limit function of staircase $S$ together with $U$ and $X$ iff $S$ is staircase sequence of $U$ in $X$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$. +\end{definition} + + +\begin{proposition}\label{naturals_in_transitive} + $\naturals$ is a \in-transitive set. +\end{proposition} +\begin{proof} + Follows by \cref{nat_is_transitiveset}. +\end{proof} + +\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{proof} + Follows by \cref{notin_emptyset}. +\end{proof} + +\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{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{naturals_is_zero_one_or_greater} + $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{naturals_one_zero_or_greater} + For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$. +\end{proposition} +\begin{proof} + Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}. +\end{proof} + +\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$. + + \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} + \caseOf{$\suc{m}=n$.} + \caseOf{$\suc{m}\neq n$.} + \begin{byCase} + \caseOf{$n = \zero$.} + \caseOf{$n \neq \zero$.} + Take $l \in \naturals$ such that $\suc{l} = n$. + Omitted. + + \end{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{bijection_naturals_order} + For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{naturals_suc_injective} + Suppose $n,m \in \naturals$. + $n = m$ iff $\suc{n} = \suc{m}$. +\end{lemma} + +\begin{lemma}\label{naturals_rless_implies_not_eq} + Suppose $n,m \in \naturals$. + Suppose $n < m$. + Then $n \neq m$. +\end{lemma} + +\begin{lemma}\label{cardinality_of_singleton} + For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$. +\end{lemma} +\begin{proof} + Omitted. + %Fix $x$. + %Suppose $x \neq \emptyset$. + %Let $X = \{x\}$. + %$\seq{\zero}{\zero}=1$. + %$\seq{\zero}{\zero}$ has cardinality $1$. + %$X \setminus \{x\} = \emptyset$. + %$1 = \{\emptyset\}$. + %Let $F = \{(x,\emptyset)\}$. + %$F$ is a relation. + %$\dom{F} = X$. + %$\emptyset \in \ran{F}$. + %for all $x \in 1$ we have $x = \emptyset$. + %$\ran{F} = 1$. + %$F$ is injective. + %$F \in \surj{X}{1}$. + %$F$ is a bijection from $X$ to $1$. +\end{proof} + +\begin{lemma}\label{cardinality_n_plus_1} + For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{cardinality_n_m_plus} + For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{cardinality_plus_disjoint} + Suppose $X \inter Y = \emptyset$. + Suppose $X$ is finite. + Suppose $Y$ is finite. + Suppose $X$ has cardinality $n$. + Suppose $Y$ has cardinality $m$. + Then $X \union Y$ has cardinality $m+n$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + + + + +\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1} + Suppose $f$ is a bijection from $X$ to $Y$. + Suppose $g$ is a function from $X$ to $Y$. + Suppose $g$ is injective. + Suppose $X$ is finite and $Y$ is finite. + For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$. +\end{lemma} +\begin{proof}[Proof by \in-induction on $n$] + Assume $n \in \naturals$. + Suppose $Y$ has cardinality $n$. + $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}. + \begin{byCase} + \caseOf{$n = \zero$.} + Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}. + \caseOf{$n \neq \zero$.} + %Take $n' \in n$ such that $n = \suc{n'}$. + %$n' \in \naturals$. + %$n' + 1 = n$. + %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. + %Let $Y' = Y \setminus \{y\}$. + %$Y' \subseteq Y$. + %$Y'$ is finite. + %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$. + %Take $m \in \naturals$ such that $Y'$ has cardinality $m$. + %Then $Y'$ has cardinality $n'$. + %Let $x' = \apply{\converse{f}}{y'}$. + %$x' \in X$. + %Let $X' = X \setminus \{x'\}$. + %$X' \subseteq X$. + %$X'$ is finite. + %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$. + %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$. + %Then $X'$ has cardinality $n'$. + %Let $f'(z)=f(z)$ for $z \in X'$. + %$\dom{f'} = X'$. + %$\ran{f'} = Y'$. + %$f'$ is a bijection from $X'$ to $Y'$. + %Let $g'(z) = g(z)$ for $z \in X'$. + %Then $g'$ is injective. + %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}. + %Define $G : X \to Y$ such that $G(z)= + %\begin{cases} + % g'(z) & \text{if} z \in X' \\ + % y' & \text{if} z = x' + %\end{cases}$ + %$G = g$. + %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}. + Omitted. + \end{byCase} + %$\converse{f}$ is a bijection from $Y$ to $X$. + %Let $h = g \circ \converse{f}$. + %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}. + %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}. +% + %Fix $y \in Y$. + %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$. + +\end{proof} + +\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection} + Suppose $f$ is a bijection from $X$ to $Y$. + Suppose $g$ is a function from $X$ to $Y$. + Suppose $g$ is injective. + Suppose $Y$ is finite. + Then $g$ is a bijection from $X$ to $Y$. +\end{lemma} +\begin{proof} + There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}. + Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}. +\end{proof} + + + +\begin{lemma}\label{naturals_bijection_implies_eq} + Suppose $n,m \in \naturals$. + Suppose $f$ is a bijection from $n$ to $m$. + Then $n = m$. +\end{lemma} +\begin{proof} + $n$ is finite. + $m$ is finite. + Suppose not. + Then $n < m$ or $m < n$. + \begin{byCase} + \caseOf{$n < m$.} + Then $n \in m$. + There exist $x \in m$ such that $x \notin n$. + $\identity{n}$ is a function from $n$ to $m$. + $\identity{n}$ is injective. + $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. + Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. + \caseOf{$m < n$.} + Then $m \in n$. + There exist $x \in n$ such that $x \notin m$. + $\converse{f}$ is a bijection from $m$ to $n$. + $\identity{m}$ is a function from $m$ to $n$. + $\identity{m}$ is injective. + $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}. + Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}. + \end{byCase} +\end{proof} + +\begin{lemma}\label{naturals_eq_iff_bijection} + Suppose $n,m \in \naturals$. + $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$. +\end{lemma} +\begin{proof} + We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$. + \begin{subproof} + Trivial. + \end{subproof} + We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$. + \begin{subproof}%[Proof by \in-induction on $k$] + %Assume $k \in \naturals$. + %\begin{byCase} + % \caseOf{$k = \zero$.} + % Trivial. + % \caseOf{$k \neq \zero$.} + % \begin{byCase} + % \caseOf{$m = \zero$.} + % Trivial. + % \caseOf{$m \neq \zero$.} + % Take $k' \in \naturals$ such that $\suc{k'} = k$. + % Then $k' \in k$. + % Take $m' \in \naturals$ such that $m = \suc{m'}$. + % Then $m' \in m$. + % + % \end{byCase} + %\end{byCase} + \end{subproof} +\end{proof} + +\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border} + Suppose $n,m \in \naturals$. + Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. + Then $n = m$. +\end{lemma} +\begin{proof} + We have $\seq{\zero}{n} = \suc{n}$. + Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$. + Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}. +\end{proof} + +\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq} + Suppose $n,m \in \naturals$. + Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$. + Then $\seq{\zero}{n} = \seq{\zero}{m}$. +\end{lemma} + +\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. + Suppose $U$ is inhabited. + Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered. +\end{proposition} +\begin{proof} + Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}. + \begin{byCase} + \caseOf{$n = \zero$.} + Omitted. + \caseOf{$n \neq \zero$.} + Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. + We have $\dom{U} \subseteq \naturals$. + $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}. + $\dom{U}$ has cardinality $\suc{k}$. + We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. + \begin{subproof} + For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$. + We have $\dom{U} \subseteq \naturals$. + $\dom{U}$ is inhabited. + Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. + Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. + Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$. + $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}. + $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}. + %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$. + %\begin{subproof} + % We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$. + % \begin{subproof} + % It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$. + % Fix $y \in \seq{\emptyset}{k'}$. + % Then $y \leq k'$. + % Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}. + % + % Therefore $y \in \suc{k}$. + % Therefore $y \in \seq{\emptyset}{k}$. + % \end{subproof} + % We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$. + % \begin{subproof} + % Fix $y \in \seq{\emptyset}{k}$. + % \end{subproof} + %\end{subproof} + \end{subproof} + Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$. + Let $N = \seq{\zero}{k}$. + Let $M = \pow{X}$. + Define $V : N \to M$ such that $V(n)= + \begin{cases} + \at{U}{F(n)} & \text{if} n \in N + \end{cases}$ + $\dom{V} = \seq{\zero}{k}$. + We show that $V$ is a urysohnchain of $X$. + \begin{subproof} + It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$. + We show that $V$ is a chain of subsets in $X$. + \begin{subproof} + It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$. + $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}. + It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$. + Fix $n \in \dom{V}$. + Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$. + Fix $m$ such that $m \in \dom{V}$ and $n \rless m$. + Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + \end{subproof} + It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$. + Fix $n \in \dom{V}$. + Fix $m$ such that $m \in \dom{V} \land n \rless m$. + Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + \end{subproof} + We show that $F$ is consistent on $V$ to $U$. + \begin{subproof} + It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}. + $F$ is a bijection from $\dom{V}$ to $\dom{U}$. + It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$. + Fix $n \in \dom{V}$. + Fix $m$ such that $m \in \dom{V}$ and $n \rless m$. + Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}. + \end{subproof} + $V$ is normal ordered. + \end{byCase} + +\end{proof} + + +\begin{proposition}\label{staircase_ran_in_zero_to_one} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain of $X$. + Suppose $f$ is a staircase function adapted to $U$ in $X$. + Then $\ran{f} \subseteq \intervalclosed{\zero}{1}$. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\begin{proposition}\label{staircase_limit_is_continuous} + Let $X$ be a urysohn space. + Suppose $U$ is a lifted urysohnchain of $X$. + Suppose $S$ is staircase sequence of $U$ in $X$. + Suppose $f$ is the limit function of staircase $S$ together with $U$ and $X$. + Then $f$ is continuous. +\end{proposition} +\begin{proof} + Omitted. +\end{proof} + +\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{lemma}\label{fractions_between_zero_one} + Suppose $n,m \in \naturals$. + Suppose $m > n$. + Then $\zero \leq \rfrac{n}{m} \leq 1$. +\end{lemma} +\begin{proof} + Omitted. +\end{proof} + +\begin{lemma}\label{intervalclosed_border_is_elem} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then $a,b \in \intervalclosed{a}{b}$. +\end{lemma} + +\begin{lemma}\label{urysohnchain_subseteqrel} + Let $X$ be a urysohn space. + Suppose $U$ is a urysohnchain of $X$. + Then for all $n,m \in \dom{U}$ such that $n < m$ we have $\at{U}{n} \subseteq \at{U}{m}$. +\end{lemma} + + +\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$ is continuous + and for all $a,b$ such that $a \in A$ and $b \in B$ we have $f(a)= \zero$ and $f(b) = 1$. +\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$. + + We show that there exist $S$ such that $S$ is staircase sequence of $U$ in $X$. + \begin{subproof} + Omitted. + \end{subproof} + Take $S$ such that $S$ is staircase sequence of $U$ in $X$. + + %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$. +% + %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for . + We show that there exist $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$. + \begin{subproof} + Omitted. + \end{subproof} + Take $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$. + Then $f$ is continuous. + We show that $\dom{f} = \carrier[X]$. + \begin{subproof} + Trivial. + \end{subproof} + $f$ is a function. + We show that $\ran{f} \subseteq \intervalclosed{\zero}{1}$. + \begin{subproof} + It suffices to show that $f$ is a function to $\intervalclosed{\zero}{1}$. + It suffices to show that for all $x \in \dom{f}$ we have $f(x) \in \intervalclosed{\zero}{1}$. + Fix $x \in \dom{f}$. + $f(x)$ is the staircase limit of $S$ with $x$. + Therefore $f(x) \in \reals$. + + We show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. + \begin{subproof} + Fix $n \in \naturals$. + Let $g = \at{S}{n}$. + Let $U' = \at{U}{n}$. + $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + $g$ is a staircase function adapted to $U'$ in $X$. + $U'$ is a urysohnchain of $X$. + $g$ is a function from $\carrier[X]$ to $\reals$. + It suffices to show that $\ran{g} \subseteq \intervalclosed{\zero}{1}$ by \cref{function_apply_default,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,function_apply_elim,inter,inter_absorb_supseteq_left,ran_iff,funs_is_relation,funs_is_function,staircase2}. + 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]$. + \begin{byCase} + \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.} + Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$. + We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$. + \begin{subproof} + Omitted. + \end{subproof} + Therefore $x \notin (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$. + We show that $g(x) = 1$. + \begin{subproof} + Omitted. + \end{subproof} + \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.} + \begin{byCase} + \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.} + We show that $g(x) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} + \caseOf{$x \in (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.} + Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$. + Omitted. + \end{byCase} + \end{byCase} + + + + %$\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + %$\at{U}{n}$ is a urysohnchain of $X$. + %$\at{S}{n}$ is a function from $\carrier[X]$ to $\reals$. + %there exist $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$. + %Take $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$. + %\begin{byCase} + % \caseOf{$x \in \carrier[X] \setminus \at{\at{U}{n}}{k}$.} + % $1 \in \intervalclosed{\zero}{1}$. + % We show that for all $y \in (\carrier[X] \setminus \at{\at{U}{n}}{k})$ we have $\apply{\at{S}{n}}{y} = 1$. + % \begin{subproof} + % Omitted. + % \end{subproof} + % Then $\apply{\at{S}{n}}{x} = 1$. + % \caseOf{$x \notin \carrier[X] \setminus \at{\at{U}{n}}{k}$.} + % %There exist $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$. + % Take $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$. + % Then $\apply{\at{S}{n}}{x} = \rfrac{m'}{k'}$. + % It suffices to show that $\rfrac{m'}{k'} \in \intervalclosed{\zero}{1}$. + % $\zero \leq m' \leq k$. + %\end{byCase} + %%It suffices to show that $\zero \leq \apply{\at{S}{n}}{x} \leq 1$. + %%It suffices to show that $\ran{\at{S}{n}} \subseteq \intervalclosed{\zero}{1}$. + \end{subproof} + + Suppose not. + Then $f(x) < \zero$ or $f(x) > 1$ by \cref{reals_order_total,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,one_in_reals}. + For all $\epsilon \in \realsplus$ we have there exist $m \in \naturals$ such that $\apply{\at{S}{m}}{x} \in \epsBall{f(x)}{\epsilon}$ by \cref{plus_one_order,naturals_is_equal_to_two_times_naturals,subseteq,naturals_subseteq_reals,staircase_limit_point}. + \begin{byCase} + \caseOf{$f(x) < \zero$.} + Let $\delta = \zero - f(x)$. + $\delta \in \realsplus$. + It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$. + Fix $n \in \naturals$. + $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + For all $y \in \epsBall{f(x)}{\delta}$ we have $y < \zero$ by \cref{epsilon_ball,minus_behavior1,minus_behavior3,minus,apply,intervalopen}. + It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. + Trivial. + \caseOf{$f(x) > 1$.} + Let $\delta = f(x) - 1$. + $\delta \in \realsplus$. + It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$. + Fix $n \in \naturals$. + $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$. + For all $y \in \epsBall{f(x)}{\delta}$ we have $y > 1$ by \cref{epsilon_ball,reals_addition_minus_behavior2,minus_in_reals,apply,reals_addition_minus_behavior1,minus,reals_add,realsplus_in_reals,one_in_reals,reals_axiom_kommu,intervalopen}. + It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$. + Trivial. + \end{byCase} + + \end{subproof} + Therefore $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ by \cref{staircase_limit_function,surj_to_fun,fun_to_surj,neq_witness,inters_of_ordinals_elem,times_tuple_elim,img_singleton_iff,foundation,subseteq_emptyset_iff,inter_eq_left_implies_subseteq,inter_emptyset,funs_intro,fun_ran_iff,not_in_subseteq}. + + We show that for all $a \in A$ we have $f(a) = \zero$. + \begin{subproof} + Omitted. + \end{subproof} + We show that for all $b \in B$ we have $f(b) = 1$. + \begin{subproof} + Omitted. + \end{subproof} + + +\end{proof} + +%\begin{theorem}\label{safe} +% Contradiction. +%\end{theorem} + + + + + + -- cgit v1.2.3