diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/topology/real-topological-space.tex | 121 | ||||
| -rw-r--r-- | library/topology/urysohn.tex | 515 | ||||
| -rw-r--r-- | library/topology/urysohn2.tex | 14 |
3 files changed, 367 insertions, 283 deletions
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index 1c5e4cb..ffdf46e 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -11,7 +11,7 @@ \import{function.tex} -\section{The canonical topology on $\mathbbR$} +\section{The canonical topology on $\mathbb{R}$} \begin{definition}\label{topological_basis_reals_eps_ball} $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$. @@ -101,12 +101,15 @@ For all $x,y \in \reals$ such that $x < y$ we have there exists $z \in \realsplus$ such that $x + z = y$. \end{lemma} \begin{proof} - %Fix $x,y \in \reals$. + Omitted. \end{proof} \begin{lemma}\label{reals_order_is_transitive} For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$. \end{lemma} +\begin{proof} + Omitted. +\end{proof} \begin{lemma}\label{reals_order_plus_minus} Suppose $a,b \in \reals$. @@ -134,16 +137,9 @@ $x + \epsilon \in \reals$. - %It suffices to show that for all $c$ such that $c \rless x$ we have $c \in \epsBall{x}{\epsilon}$. - %Fix $c$ such that $c \rless x$. -% - %It suffices to show that for all $c$ such that $c < x$ we have $c \in \epsBall{x}{\epsilon}$. - %Fix $c$ such that $c < x$. - - It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$. Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$. - %Suppose $(x - \epsilon) < c < (x + \epsilon)$. + $(x - \epsilon) < c < (x + \epsilon)$. \end{proof} \begin{theorem}\label{topological_basis_reals_is_prebasis} @@ -158,9 +154,9 @@ \caseOf{$x = \emptyset$.} Trivial. \caseOf{$x \neq \emptyset$.} - There exists $U \in \topoBasisReals$ such that $x \in \topoBasisReals$. - Take $U \in \topoBasisReals$ such that $x \in \topoBasisReals$. - + %There exists $U \in \topoBasisReals$ such that $x \in U$. + Take $U \in \topoBasisReals$ such that $x \in U$. + Follows by \cref{epsball_are_subseteq_reals_set,topological_basis_reals_eps_ball,epsilon_ball,minus,subseteq}. \end{byCase} \end{subproof} We show that $\reals \subseteq \unions{\topoBasisReals}$. @@ -168,10 +164,63 @@ It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$. Fix $x \in \reals$. $\epsBall{x}{1} \in \topoBasisReals$. - Therefore $x \in \unions{\topoBasisReals}$. + Therefore $x \in \unions{\topoBasisReals}$ by \cref{one_in_reals,reals_one_bigger_zero,unions_intro,realsplus,plus_one_order,reals_order_minus_positiv,epsball_are_connected_in_reals}. \end{subproof} \end{proof} +%\begin{lemma}\label{intervl_intersection_is_interval} +% Suppose $a,b,a',b' \in \reals$. +% Suppose there exist $x \in \reals$ such that $x \in \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$. +% Then there exists $q,p \in \reals$ such that $q < p$ and $\intervalopen{q}{p} \subseteq \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$. +%\end{lemma} +% + +\begin{lemma}\label{reals_order_total} + For all $x,y \in \reals$ we have either $x < y$ or $x \geq y$. +\end{lemma} +\begin{proof} + It suffices to show that for all $x \in \reals$ we have for all $y \in \reals$ we have either $x < y$ or $x \geq y$. + Fix $x \in \reals$. + Fix $y \in \reals$. + Omitted. +\end{proof} + +\begin{lemma}\label{topo_basis_reals_eps_iff} + $X \in \topoBasisReals$ iff there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} = X$. +\end{lemma} + +\begin{lemma}\label{topo_basis_reals_intro} +For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have $\epsBall{x}{\delta} \in \topoBasisReals$. +\end{lemma} + +\begin{lemma}\label{realspuls_in_reals_plus} + For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$. +\end{lemma} + +\begin{lemma}\label{realspuls_in_reals_minus} + For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x - y \in \reals$. +\end{lemma} + +\begin{lemma}\label{eps_ball_implies_open_interval} + Suppose $x \in \reals$. + Suppose $\epsilon \in \realsplus$. + Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. +\end{lemma} + +\begin{lemma}\label{open_interval_eq_eps_ball} + Suppose $a,b \in \reals$. + Suppose $a < b$. + Then there exist $x,\epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$. +\end{lemma} +\begin{proof} + Let $\delta = (b-a)$. + $\delta$ is positiv by \cref{minus_}. + There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$. + +\end{proof} + + + \begin{theorem}\label{topological_basis_reals_is_basis} $\topoBasisReals$ is a topological basis for $\reals$. \end{theorem} @@ -188,7 +237,45 @@ Trivial. \caseOf{$U \inter V \neq \emptyset$.} Then $U \inter V$ is inhabited. - %It suffices to show that + $x \in \reals$ by \cref{inter_lower_left,subseteq,topological_prebasis_iff_covering_family,omega_is_an_ordinal,naturals_subseteq_reals,subset_transitive,suc_subseteq_elim,ordinal_suc_subseteq}. + There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$. + There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$. + Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$. + Then $ (x_2 - \beta) < x < (x_2 + \beta)$. + We show that if there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$ then there exists $W\in B$ such that $x\in W\subseteq U, V$. + \begin{subproof} + Suppose there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$. + $x \in \epsBall{x}{\delta}$. + $\epsBall{x}{\delta} \subseteq U$. + $\epsBall{x}{\delta} \subseteq V$. + $\epsBall{x}{\delta} \in B$. + \end{subproof} + It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$. + + + %It suffices to show that there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} \subseteq u \inter V$. + %There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$. + %There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$. + %Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$. + %Then $ (x_2 - \beta) < x < (x_2 + \beta)$. + %\begin{byCase} + % \caseOf{$x_1 = x_2$.} + % Take $\gamma \in \realsplus$ such that either $\gamma = \alpha \land \gamma \leq \beta$ or $\gamma \leq \alpha \land \gamma = \beta$. + % \caseOf{$x_1 < x_2$.} + % \caseOf{$x_1 > x_2$.} + %\end{byCase} + %%Take $m$ such that $m \in \min{\{(x_1 + \alpha), (x_2 + \beta)\}}$. + %Take $n$ such that $n \in \max{\{(x_1 - \alpha), (x_2 - \beta)\}}$. + %Then $m < x < n$. + %We show that there exists $x_1 \in \reals$ such that $x_1 \in U \inter V$ and $x_1 < x$. + %\begin{subproof} + % Suppose not. + % Then For all $y \in U \inter V$ we have $x \leq y$. + %\end{subproof} + %We show that there exists $x_2 \in \reals$ such that $x_2 \in U \inter V$ and $x_2 > x$. + %\begin{subproof} + % Trivial. + %\end{subproof} \end{byCase} \end{proof} @@ -230,7 +317,3 @@ Suppose $a,b \in \reals$. Then $\intervalopen{a}{b} \in \opens[\reals]$. \end{proposition} - -\begin{lemma}\label{safetwo} - Contradiction. -\end{lemma}
\ No newline at end of file diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 17e2911..ff6a231 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -51,13 +51,14 @@ The first tept will be a formalisation of chain constructions. \begin{struct}\label{sequence} A sequence $X$ is a onesorted structure equipped with \begin{enumerate} - \item $\index$ - \item $\indexset$ + \item $\indexx$ + \item $\indexxset$ + \end{enumerate} such that \begin{enumerate} - \item\label{indexset_is_subset_naturals} $\indexset[X] \subseteq \naturals$. - \item\label{index_is_bijection} $\index[X]$ is a bijection from $\indexset[X]$ to $\carrier[X]$. + \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$. + \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$. \end{enumerate} \end{struct} @@ -68,13 +69,13 @@ The first tept will be a formalisation of chain constructions. \begin{definition}\label{cahin_of_subsets} $C$ is a chain of subsets iff - $C$ is a sequence and for all $n,m \in \indexset[C]$ such that $n < m$ we have $\index[C](n) \subseteq \index[C](m)$. + $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$. \end{definition} \begin{definition}\label{chain_of_n_subsets} $C$ is a chain of $n$ subsets iff - $C$ is a chain of subsets and $n \in \indexset[C]$ - and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexset[C]$. + $C$ is a chain of subsets and $n \in \indexxset[C]$ + and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$. \end{definition} @@ -133,18 +134,18 @@ The first tept will be a formalisation of chain constructions. \item \label{staircase_domain} $\dom{f}$ is a topological space. \item \label{staricase_def_chain} $C$ is a chain of subsets. \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. - \item \label{staircase_behavoir_index_zero} $f(\index[C](1))= 1$. + \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. - \item \label{staircase_chain_indeset} There exist $n$ such that $\indexset[C] = \seq{\zero}{n}$. - \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexset[C]$ - such that $n \neq \zero$ we have $f(\index[C](n) \setminus \index[C](n-1)) = \rfrac{n}{ \max{\indexset[C]} }$. + \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$. + \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ + such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. \end{enumerate} \end{struct} \begin{definition}\label{legal_staircase} $f$ is a legal staircase function iff $f$ is a staircase function and - for all $n,m \in \indexset[\chain[f]]$ such that $n \leq m$ we have $f(\index[\chain[f]](n)) \leq f(\index[\chain[f]](m))$. + for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$. \end{definition} \begin{abbreviation}\label{urysohnspace} @@ -159,23 +160,23 @@ The first tept will be a formalisation of chain constructions. $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused! $C$ is a chain of subsets and for all $A \in C$ we have $A \subseteq X$ and - for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. + for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$. \end{definition} \begin{definition}\label{urysohnchain_without_cardinality} $C$ is a urysohnchain in $X$ iff $C$ is a chain of subsets and for all $A \in C$ we have $A \subseteq X$ and - for all $n,m \in \indexset[C]$ such that $n < m$ we have $\closure{\index[C](n)}{X} \subseteq \interior{\index[C](m)}{X}$. + for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$. \end{definition} \begin{abbreviation}\label{infinte_sequence} - $S$ is a infinite sequence iff $S$ is a sequence and $\indexset[S]$ is infinite. + $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite. \end{abbreviation} \begin{definition}\label{infinite_product} $X$ is the infinite product of $Y$ iff - $X$ is a infinite sequence and for all $i \in \indexset[X]$ we have $\index[X](i) = Y$. + $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$. \end{definition} \begin{definition}\label{refinmant} @@ -289,9 +290,9 @@ The first tept will be a formalisation of chain constructions. Suppose $A \inter B$ is empty. Then there exist $U$ such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ - and $\indexset[U]= \{\zero, 1\}$ - and $\index[U](\zero) = A$ - and $\index[U](1) = (\carrier[X] \setminus B)$. + and $\indexxset[U]= \{\zero, 1\}$ + and $\indexx[U](\zero) = A$ + and $\indexx[U](1) = (\carrier[X] \setminus B)$. %$U$ is a urysohnchain in $X$. \end{proposition} \begin{proof} @@ -310,12 +311,12 @@ The first tept will be a formalisation of chain constructions. % % We show that $U$ is a chain of subsets. % \begin{subproof} - % For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$. - % It suffices to show that for all $n \in \indexset[U]$ we have - % for all $m \in \indexset[U]$ such that - % $n < m$ we have $\index[U](n) \subseteq \index[U](m)$. - % Fix $n \in \indexset[U]$. - % Fix $m \in \indexset[U]$. + % For all $n \in \indexxset[U]$ we have $n = \zero \lor n = 1$. + % It suffices to show that for all $n \in \indexxset[U]$ we have + % for all $m \in \indexxset[U]$ such that + % $n < m$ we have $\indexx[U](n) \subseteq \indexx[U](m)$. + % Fix $n \in \indexxset[U]$. + % Fix $m \in \indexxset[U]$. % \begin{byCase} % \caseOf{$n = 1$.} Trivial. % \caseOf{$n = \zero$.} @@ -337,8 +338,8 @@ The first tept will be a formalisation of chain constructions. % \begin{subproof} % Omitted. % \end{subproof} - % We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have - % $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$. + % We show that for all $n,m \in \indexxset[U]$ such that $n < m$ we have + % $\closure{\indexx[U](n)}{X} \subseteq \interior{\indexx[U](m)}{X}$. % \begin{subproof} % Omitted. % \end{subproof} @@ -352,9 +353,9 @@ The first tept will be a formalisation of chain constructions. Suppose $A \inter B$ is empty. Suppose there exist $U$ such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$ - and $\indexset[U]= \{\zero, 1\}$ - and $\index[U](\zero) = A$ - and $\index[U](1) = (\carrier[X] \setminus B)$. + and $\indexxset[U]= \{\zero, 1\}$ + and $\indexx[U](\zero) = A$ + and $\indexx[U](1) = (\carrier[X] \setminus B)$. Then $U$ is a urysohnchain in $X$. \end{proposition} \begin{proof} @@ -384,9 +385,9 @@ The first tept will be a formalisation of chain constructions. % U = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n}) % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ... A_{n-1}, A'_{n}, A_{n}) - % Let $m = \max{\indexset[U]}$. - % For all $n \in (\indexset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ - % such that $\closure{\index[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\index[U](n+1)}{X}$. + % Let $m = \max{\indexxset[U]}$. + % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ + % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$. %\begin{definition}\label{refinmant} @@ -408,7 +409,7 @@ The first tept will be a formalisation of chain constructions. Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$. Suppose $k \neq \zero$. Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ + and for all $n \in \indexxset[U]$ we have for all $x \in \indexx[U](n)$ we have $f(x) = \rfrac{n}{k}$. \end{proposition} \begin{proof} @@ -445,11 +446,11 @@ The first tept will be a formalisation of chain constructions. \begin{abbreviation}\label{converge} $s$ converges iff $s$ is a sequence of real numbers - and $\indexset[s]$ is infinite + and $\indexxset[s]$ is infinite and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have - there exist $N \in \indexset[s]$ such that - for all $m \in \indexset[s]$ such that $m > N$ - we have $\abs{\index[s](N) - \index[s](m)} < \epsilon$. + there exist $N \in \indexxset[s]$ such that + for all $m \in \indexxset[s]$ such that $m > N$ + we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$. \end{abbreviation} @@ -457,9 +458,9 @@ The first tept will be a formalisation of chain constructions. $x$ is the limit of $s$ iff $s$ is a sequence of real numbers and $x \in \reals$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ - we have there exist $n \in \indexset[s]$ such that - for all $m \in \indexset[s]$ such that $m > n$ - we have $\abs{x - \index[s](n)} < \epsilon$. + we have there exist $n \in \indexxset[s]$ such that + for all $m \in \indexxset[s]$ such that $m > n$ + we have $\abs{x - \indexx[s](n)} < \epsilon$. \end{definition} \begin{proposition}\label{existence_of_limit} @@ -473,9 +474,9 @@ The first tept will be a formalisation of chain constructions. \begin{definition}\label{limit_sequence} $x$ is the limit sequence of $f$ iff - $x$ is a sequence and $\indexset[x] = \dom{f}$ and - for all $n \in \indexset[x]$ we have - $\index[x](n) = f(n)$. + $x$ is a sequence and $\indexxset[x] = \dom{f}$ and + for all $n \in \indexxset[x]$ we have + $\indexx[x](n) = f(n)$. \end{definition} \begin{definition}\label{realsminus} @@ -596,15 +597,15 @@ The first tept will be a formalisation of chain constructions. \begin{proof} There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ - and $\indexset[\eta] = \{\zero, 1\}$ - and $\index[\eta](\zero) = A$ - and $\index[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnchain_induction_begin}. + and $\indexxset[\eta] = \{\zero, 1\}$ + and $\indexx[\eta](\zero) = A$ + and $\indexx[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnchain_induction_begin}. We show that there exist $\zeta$ such that $\zeta$ is a sequence - and $\indexset[\zeta] = \naturals$ - and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$ - and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ - and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$. + and $\indexxset[\zeta] = \naturals$ + and $\eta \in \carrier[\zeta]$ and $\indexx[\zeta](\eta) = \zero$ + and for all $n \in \indexxset[\zeta]$ we have $n+1 \in \indexxset[\zeta]$ + and $\indexx[\zeta](n+1)$ is a refinmant of $\indexx[\zeta](n)$. \begin{subproof} %Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$. %Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$. @@ -614,7 +615,7 @@ The first tept will be a formalisation of chain constructions. %$\dom{\beta} = \naturals$. %$\ran{\beta} = \alpha$. %$\beta \in \funs{\naturals}{\alpha}$. - %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexset[\zeta] = \naturals$ and $\index[\zeta] = \beta$. + %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexxset[\zeta] = \naturals$ and $\indexx[\zeta] = \beta$. Omitted. \end{subproof} @@ -628,14 +629,14 @@ The first tept will be a formalisation of chain constructions. %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that %$k(x)$ - %For all $n \in \naturals$ we have $\index[\zeta](n)$ is a urysohnchain in $X$. + %For all $n \in \naturals$ we have $\indexx[\zeta](n)$ is a urysohnchain in $X$. - We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. + We show that for all $n \in \indexxset[\zeta]$ we have $\indexx[\zeta](n)$ has cardinality $\pot(n)$. \begin{subproof} Omitted. \end{subproof} - We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. + We show that for all $m \in \indexxset[\zeta]$ we have $\pot(m) \neq \zero$. \begin{subproof} Omitted. \end{subproof} @@ -646,212 +647,212 @@ The first tept will be a formalisation of chain constructions. \end{subproof} - We show that for all $m \in \indexset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and for all $n \in \indexset[\index[\zeta](m)]$ we have for all $x \in \index[\index[\zeta](m)](n)$ such that $x \notin \index[\index[\zeta](m)](n-1)$ - we have $f(x) = \rfrac{n}{\pot(m)}$. - \begin{subproof} - Fix $m \in \indexset[\zeta]$. - %$\index[\zeta](m)$ is a urysohnchain in $X$. - - %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$ - %\begin{cases} - % & 0 & \text{if} x \in A - % & 1 & \text{if} x \in B - % & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \index[\index[\zeta](m)](n) \land x \notin \index[\index[\zeta](m)](n-1) - %\end{cases} +% We show that for all $m \in \indexxset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ +% and for all $n \in \indexxset[\indexx[\zeta](m)]$ we have for all $x \in \indexx[\indexx[\zeta](m)](n)$ such that $x \notin \indexx[\indexx[\zeta](m)](n-1)$ +% we have $f(x) = \rfrac{n}{\pot(m)}$. +% \begin{subproof} +% Fix $m \in \indexxset[\zeta]$. +% %$\indexx[\zeta](m)$ is a urysohnchain in $X$. % - Omitted. - \end{subproof} - - - - %The sequenc of the functions - Let $\gamma = \{ - (n,f) \mid - n \in \naturals \mid - - \forall n' \in \indexset[\index[\zeta](n)]. - \forall x \in \carrier[X]. - - - f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land - - - % (n,f) \in \gamma <=> \phi(n,f) - % with \phi (n,f) := - % (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n ) - % \/ (x \notin A_k for all k \in {1,..,n} ==> f(x) = 1 - - ( (n' = \zero) - \land (x \in \index[\index[\zeta](n)](n')) - \land (f(x)= \zero) ) - - \lor - - ( (n' > \zero) - \land (x \in \index[\index[\zeta](n)](n')) - \land (x \notin \index[\index[\zeta](n)](n'-1)) - \land (f(x) = \rfrac{n'}{\pot(n)}) ) - - \lor - - ( (x \notin \index[\index[\zeta](n)](n')) - \land (f(x) = 1) ) - - \}$. - - Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. - - We show that for all $n \in \naturals$ we have $\gamma(n)$ - is a function from $\carrier[X]$ to $\reals$. - \begin{subproof} - Omitted. - \end{subproof} - - - We show that for all $n \in \naturals$ we have $\gamma(n)$ - is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$. - \begin{subproof} - Omitted. - \end{subproof} - - We show that $\gamma$ is a function from $\naturals$ to $\reals$. - \begin{subproof} - Omitted. - \end{subproof} - - We show that for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \index[\index[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} = \rfrac{k}{\pot(n)}$. - \begin{subproof} - Omitted. - \end{subproof} - - We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. - \begin{subproof} - Fix $n \in \naturals$. - Fix $x \in \carrier[X]$. - Omitted. - \end{subproof} - - - - We show that - if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ - then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$. - \begin{subproof} - Omitted. - \end{subproof} - - - - We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. - \begin{subproof} - We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. - \begin{subproof} - Fix $x \in \carrier[X]$. - - Omitted. - - % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. - %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. - \end{subproof} - Omitted. - \end{subproof} - - - Let $G(x) = g(x)$ for $x \in \carrier[X]$. - We have $\dom{G} = \carrier[X]$. - - We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$. - \begin{subproof} - %Fix $x \in \dom{G}$. - %It suffices to show that $g(x) \in \reals$. +% %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$ +% %\begin{cases} +% % & 0 & \text{if} x \in A +% % & 1 & \text{if} x \in B +% % & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \indexx[\indexx[\zeta](m)](n) \land x \notin \indexx[\indexx[\zeta](m)](n-1) +% %\end{cases} +%% +% Omitted. +% \end{subproof} % - %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +% % - %We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$. - %\begin{subproof} - % Fix $\epsilon \in \reals$. - % +% %The sequenc of the functions +% Let $\gamma = \{ +% (n,f) \mid +% n \in \naturals \mid +% +% \forall n' \in \indexxset[\indexx[\zeta](n)]. +% \forall x \in \carrier[X]. +% % - %\end{subproof} - %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}. - Omitted. - \end{subproof} - - We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. - \begin{subproof} - %Fix $x \in \dom{G}$. - %Then $x \in \carrier[X]$. - %\begin{byCase} - % \caseOf{$x \in A$.} - % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$. -% -% - % \caseOf{$x \notin A$.} - % \begin{byCase} - % \caseOf{$x \in B$.} - % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. -% - % \caseOf{$x \notin B$.} - % Omitted. - % \end{byCase} - %\end{byCase} - Omitted. - \end{subproof} - - - We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. - \begin{subproof} - %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}. - %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$. - %Fix $x \in \dom{G}$. - %Then $x \in \carrier[X]$. - %$g(x) = G(x)$. - %We have $G(x) \in \reals$. - %$\zero \leq G(x) \leq 1$. - %We have $G(x) \in \intervalclosed{\zero}{1}$ . - Omitted. - \end{subproof} - - We show that $G(A) = \zero$. - \begin{subproof} - Omitted. - \end{subproof} - - We show that $G(B) = 1$. - \begin{subproof} - Omitted. - \end{subproof} - - We show that $G$ is continuous. - \begin{subproof} - Omitted. - \end{subproof} - - %Suppose $\eta$ is a urysohnchain in $X$. - %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ - %and $\indexset[\eta] = \{\zero, 1\}$ - %and $\index[\eta](\zero) = A$ - %and $\index[\eta](1) = (X \setminus B)$. - - - %Then $\eta$ is a urysohnchain in $X$. - - % Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$. - % - % We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence - % and for all $i \in \indexset[\zeta]$ we have - % $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ - % and $A \subseteq \index[\zeta](i)$ - % and $\index[\zeta](i) \subseteq (X \setminus B)$ - % and for all $j \in \indexset[\zeta]$ such that - % $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$. - % \begin{subproof} - % Omitted. - % \end{subproof} - % - % - % +% f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land +% +% +% % (n,f) \in \gamma <=> \phi(n,f) +% % with \phi (n,f) := +% % (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n ) +% % \/ (x \notin A_k for all k \in {1,..,n} ==> f(x) = 1 +% +% ( (n' = \zero) +% \land (x \in \indexx[\indexx[\zeta](n)](n')) +% \land (f(x)= \zero) ) +% +% \lor +% +% ( (n' > \zero) +% \land (x \in \indexx[\indexx[\zeta](n)](n')) +% \land (x \notin \indexx[\indexx[\zeta](n)](n'-1)) +% \land (f(x) = \rfrac{n'}{\pot(n)}) ) +% +% \lor +% +% ( (x \notin \indexx[\indexx[\zeta](n)](n')) +% \land (f(x) = 1) ) +% +% \}$. +% +% Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. +% +% We show that for all $n \in \naturals$ we have $\gamma(n)$ +% is a function from $\carrier[X]$ to $\reals$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% +% We show that for all $n \in \naturals$ we have $\gamma(n)$ +% is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that $\gamma$ is a function from $\naturals$ to $\reals$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \indexx[\indexx[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} = \rfrac{k}{\pot(n)}$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. +% \begin{subproof} +% Fix $n \in \naturals$. +% Fix $x \in \carrier[X]$. +% Omitted. +% \end{subproof} +% +% +% +% We show that +% if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ +% then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% +% +% We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +% \begin{subproof} +% We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +% \begin{subproof} +% Fix $x \in \carrier[X]$. +% +% Omitted. +% +% % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. +% %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}. +% \end{subproof} +% Omitted. +% \end{subproof} +% +% +% Let $G(x) = g(x)$ for $x \in \carrier[X]$. +% We have $\dom{G} = \carrier[X]$. +% +% We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$. +% \begin{subproof} +% %Fix $x \in \dom{G}$. +% %It suffices to show that $g(x) \in \reals$. +%% +% %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$. +%% +% %We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$. +% %\begin{subproof} +% % Fix $\epsilon \in \reals$. +% % +%% +% %\end{subproof} +% %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}. +% Omitted. +% \end{subproof} +% +% We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$. +% \begin{subproof} +% %Fix $x \in \dom{G}$. +% %Then $x \in \carrier[X]$. +% %\begin{byCase} +% % \caseOf{$x \in A$.} +% % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$. +%% +%% +% % \caseOf{$x \notin A$.} +% % \begin{byCase} +% % \caseOf{$x \in B$.} +% % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. +%% +% % \caseOf{$x \notin B$.} +% % Omitted. +% % \end{byCase} +% %\end{byCase} +% Omitted. +% \end{subproof} +% +% +% We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. +% \begin{subproof} +% %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}. +% %It suffices to show that for all $x \in \dom{G}$ we have $G(x) \in \intervalclosed{\zero}{1}$. +% %Fix $x \in \dom{G}$. +% %Then $x \in \carrier[X]$. +% %$g(x) = G(x)$. +% %We have $G(x) \in \reals$. +% %$\zero \leq G(x) \leq 1$. +% %We have $G(x) \in \intervalclosed{\zero}{1}$ . +% Omitted. +% \end{subproof} +% +% We show that $G(A) = \zero$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that $G(B) = 1$. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% We show that $G$ is continuous. +% \begin{subproof} +% Omitted. +% \end{subproof} +% +% %Suppose $\eta$ is a urysohnchain in $X$. +% %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ +% %and $\indexxset[\eta] = \{\zero, 1\}$ +% %and $\indexx[\eta](\zero) = A$ +% %and $\indexx[\eta](1) = (X \setminus B)$. +% +% +% %Then $\eta$ is a urysohnchain in $X$. +% +% % Take $P$ such that $P$ is a infinite sequence and $\indexxset[P] = \naturals$ and for all $i \in \indexxset[P]$ we have $\indexx[P](i) = \pow{X}$. +% % +% % We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence +% % and for all $i \in \indexxset[\zeta]$ we have +% % $\indexx[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$ +% % and $A \subseteq \indexx[\zeta](i)$ +% % and $\indexx[\zeta](i) \subseteq (X \setminus B)$ +% % and for all $j \in \indexxset[\zeta]$ such that +% % $j < i$ we have for all $x \in \indexx[\zeta](j)$ we have $x \in \indexx[\zeta](i)$. +% % \begin{subproof} +% % Omitted. +% % \end{subproof} +% % +% % +% % % % % diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 838b121..83e3aa4 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -367,10 +367,10 @@ \end{subproof} Let $N = \seq{\zero}{k}$. Let $M = \pow{X}$. - Define $V : N \to M$ such that $V(n)=$ + Define $V : N \to M$ such that $V(n)= \begin{cases} - &\at{U}{F(n)} & \text{if} n \in N - \end{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} @@ -445,11 +445,11 @@ $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) =$ + 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} + 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}. |