diff options
Diffstat (limited to 'library/topology/urysohn2.tex')
| -rw-r--r-- | library/topology/urysohn2.tex | 72 |
1 files changed, 65 insertions, 7 deletions
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 83e3aa4..9990199 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -94,6 +94,9 @@ \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. @@ -119,6 +122,9 @@ \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. @@ -163,6 +169,13 @@ 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} @@ -184,7 +197,7 @@ \end{subproof} \caseOf{$n = 1$.} Fix $m$. - For all $l \in \naturals$ we have If $l < 1$ then $l = \zero$. + 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$. @@ -350,7 +363,7 @@ 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 $U$ to $V$ and $V$ is normal ordered. + 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}. @@ -360,11 +373,36 @@ \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. + $\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} - Omitted. + 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}. + 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}. + %Then $\seq{\emptyset}{k'} \in \suc{k}$. + 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)= @@ -374,11 +412,31 @@ $\dom{V} = \seq{\zero}{k}$. We show that $V$ is a urysohnchain of $X$. \begin{subproof} - Trivial. + 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 $U$ to $V$. + We show that $F$ is consistent on $V$ to $U$. \begin{subproof} - Trivial. + 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} |