diff options
Diffstat (limited to 'library/topology')
| -rw-r--r-- | library/topology/urysohn.tex | 248 |
1 files changed, 124 insertions, 124 deletions
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index cd85fbc..bfbf54d 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -13,8 +13,8 @@ \import{set/fixpoint.tex} \import{set/product.tex} -\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1} -% In this section we want to proof Urysohns lemma. +\section{Urysohns Lemma Part One with struct}\label{form_sec_urysohn1} +% In this section we want to proof Urysohns lemma. % We try to follow the proof of Klaus Jänich in his book. TODO: Book reference % The Idea is to construct staircase functions as a chain. % The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$. @@ -22,29 +22,29 @@ %Chains of sets. -This is the first attempt to prove Urysohns Lemma with the usage of struct. +This is the first attempt to prove Urysohns Lemma with the usage of struct. \subsection{Chains of sets} % Assume $A,B$ are subsets of a topological space $X$. % As Jänich propose we want a special property on chains of subsets. -% We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. +% We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. % \begin{align} -% A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B -% \end{align} -% such that for all elements in this chain following holds, -% $\overline{A_{i-1}} \subset \interior{A_{i}}$. +% A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B +% \end{align} +% such that for all elements in this chain following holds, +% $\overline{A_{i-1}} \subset \interior{A_{i}}$. % In this case we call the chain legal. \begin{definition}\label{urysohnone_one_to_n_set} - $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. + $\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$. \end{definition} %%----------------------- % Idea: -% A sequence could be define as a family of sets, +% A sequence could be define as a family of sets, % together with the existence of an indexing function. % %%----------------------- @@ -53,7 +53,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \begin{enumerate} \item $\indexx$ \item $\indexxset$ - + \end{enumerate} such that \begin{enumerate} @@ -62,7 +62,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \end{enumerate} \end{struct} -% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen +% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen @@ -74,7 +74,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \begin{definition}\label{urysohnone_chain_of_n_subsets} $C$ is a chain of $n$ subsets iff - $C$ is a chain of subsets and $n \in \indexxset[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} @@ -85,19 +85,19 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % \begin{definition}\label{urysohnone_legal_chain} -% $C$ is a legal chain of subsets of $X$ iff -% $C \subseteq \pow{X}$. %and +% $C$ is a legal chain of subsets of $X$ iff +% $C \subseteq \pow{X}$. %and % %there exist $f \in \funs{C}{\naturals}$ such that % %for all $x,y \in C$ we have if $f(x) < f(y)$ then $x \subset y \land \closure{x} \subset \interior{y}$. % \end{definition} -% TODO: We need a notion for declarinf new properties to existing thing. +% TODO: We need a notion for declarinf new properties to existing thing. % % The following gives a example and a wish want would be nice to have: % "A (structure) is called (adjectiv of property), if" % % This should then be use als follows: -% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). +% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). % Which should be translated to fol like this: % ?[X]: is_structure(X) & is_adjectiv_1(X) & ... & is_adjectiv_n(X) % --------------------------------------------------------------- @@ -134,17 +134,17 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \item \label{urysohnone_staircase_domain} $\dom{f}$ is a topological space. \item \label{urysohnone_staricase_def_chain} $C$ is a chain of subsets. \item \label{urysohnone_staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$. - \item \label{urysohnone_staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. + \item \label{urysohnone_staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. \item \label{urysohnone_staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$. \item \label{urysohnone_staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$. - \item \label{urysohnone_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]} }$. + \item \label{urysohnone_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{urysohnone_legal_staircase} $f$ is a legal staircase function iff - $f$ is a staircase function and + $f$ is a staircase function and 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} @@ -153,7 +153,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. $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$. + such that $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$. \end{abbreviation} \begin{definition}\label{urysohnone_urysohnchain} @@ -181,7 +181,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \begin{definition}\label{urysohnone_refinmant} $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$ - and for all $x \in C$ we have $x \in C'$ + and for all $x \in C$ we have $x \in C'$ and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$ and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$. \end{definition} @@ -226,7 +226,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. $\pot \in \funs{\naturals}{\naturals}$. \end{axiom} -\begin{axiom}\label{urysohnone_pot2} +\begin{axiom}\label{urysohnone_pot2} For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$. %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$. \end{axiom} @@ -267,7 +267,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. Therefore $C$ is closed in $X$ by \cref{closure_is_closed}. \begin{byCase} \caseOf{$C = B$.} - %We have $\carrier[X] \setminus A$ is open in $X$. + %We have $\carrier[X] \setminus A$ is open in $X$. %We have $\carrier[X] \setminus B$ is open in $X$. %$\{x\}$ is closed in $X$.% by \cref{hausdorff_implies_singltons_closed}. %$A \union \{x\} = C$. @@ -303,37 +303,37 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % \begin{subproof} % Omitted. % \end{subproof} -% +% % We show that $A \subseteq (\carrier[X] \setminus B)$. % \begin{subproof} % Omitted. % \end{subproof} -% +% % We show that $U$ is a chain of subsets. % \begin{subproof} % For all $n \in \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 + % 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$.} + % \caseOf{$n = \zero$.} % \begin{byCase} % \caseOf{$m = \zero$.} Trivial. % \caseOf{$m = 1$.} Omitted. % \end{byCase} % \end{byCase} % \end{subproof} -% +% % $A \subseteq X$. % $(X \setminus B) \subseteq X$. % We show that for all $x \in U$ we have $x \subseteq X$. % \begin{subproof} % Omitted. % \end{subproof} -% +% % We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$. % \begin{subproof} % Omitted. @@ -344,7 +344,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % Omitted. % \end{subproof} - + \end{proof} \begin{proposition}\label{urysohnone_urysohnchain_induction_begin_step_two} @@ -367,7 +367,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \begin{proposition}\label{urysohnone_t_four_propositon} Let $X$ be a urysohn space. Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$ - we have there exists $C \subseteq X$ such that + we have there exists $C \subseteq X$ such that $\closure{A}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{B}{X}$. \end{proposition} \begin{proof} @@ -386,13 +386,13 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ... A_{n-1}, A'_{n}, A_{n}) % Let $m = \max{\indexxset[U]}$. - % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ + % 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{urysohnone_refinmant} - % $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and - % for all $y \in C$ such that $y \subset x$ + % $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and + % for all $y \in C$ such that $y \subset x$ % we have there exist $c \in C'$ such that $y \subset c \subset x$ % and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$. %\end{definition} @@ -408,8 +408,8 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. Let $X$ be a urysohn space. Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$. Suppose $k \neq \zero$. - Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and for all $n \in \indexxset[U]$ we have for all $x \in \indexx[U](n)$ + Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ + 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} @@ -425,12 +425,12 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \begin{abbreviation}\label{urysohnone_sequence_of_functions} - $f$ is a sequence of functions iff $f$ is a sequence + $f$ is a sequence of functions iff $f$ is a sequence and for all $g \in \carrier[f]$ we have $g$ is a function. \end{abbreviation} \begin{abbreviation}\label{urysohnone_sequence_in_reals} - $s$ is a sequence of real numbers iff $s$ is a sequence + $s$ is a sequence of real numbers iff $s$ is a sequence and for all $r \in \carrier[s]$ we have $r \in \reals$. \end{abbreviation} @@ -445,27 +445,27 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \end{axiom} \begin{abbreviation}\label{urysohnone_converge} - $s$ converges iff $s$ is a sequence of real numbers + $s$ converges iff $s$ is a sequence of real numbers and $\indexxset[s]$ is infinite and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \indexxset[s]$ such that - for all $m \in \indexxset[s]$ such that $m > N$ + for all $m \in \indexxset[s]$ such that $m > N$ we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$. \end{abbreviation} \begin{definition}\label{urysohnone_limit_of_sequence} $x$ is the limit of $s$ iff $s$ is a sequence of real numbers - and $x \in \reals$ and + and $x \in \reals$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ - we have there exist $n \in \indexxset[s]$ such that - for all $m \in \indexxset[s]$ such that $m > n$ + 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{urysohnone_existence_of_limit} Let $s$ be a sequence of real numbers. - Then $s$ converges iff there exist $x \in \reals$ + Then $s$ converges iff there exist $x \in \reals$ such that $x$ is the limit of $s$. \end{proposition} \begin{proof} @@ -515,7 +515,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \begin{lemma}\label{urysohnone_frection3} Suppose $a \in \reals$. Suppose $a < \zero$. - Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. + Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. \end{lemma} \begin{proof} Omitted. @@ -560,7 +560,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. - + %\begin{definition}\label{urysohnone_sequencetwo} % $Z$ is a sequencetwo iff $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$. %\end{definition} @@ -591,20 +591,20 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. 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}}$ + There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous. \end{theorem} \begin{proof} - - There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ - and $\indexxset[\eta] = \{\zero, 1\}$ + + There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ + and $\indexxset[\eta] = \{\zero, 1\}$ and $\indexx[\eta](\zero) = A$ and $\indexx[\eta](1) = (\carrier[X] \setminus B)$ by \cref{urysohnone_urysohnchain_induction_begin}. - - We show that there exist $\zeta$ such that $\zeta$ is a sequence + + We show that there exist $\zeta$ such that $\zeta$ is a sequence 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 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\}$. @@ -622,8 +622,8 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. Let $\alpha = \carrier[X]$. %Define $f : \alpha \to \naturals$ such that $f(x) =$ %\begin{cases} - % & 1 & \text{if} x \in A \lor x \in B - % & k & \text{if} \exists k \in \naturals + % & 1 & \text{if} x \in A \lor x \in B + % & k & \text{if} \exists k \in \naturals %\end{cases} % %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that @@ -646,9 +646,9 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. Omitted. \end{subproof} - -% 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 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]$. @@ -656,61 +656,61 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % % %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 +% % & 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} % -% +% % % %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]. -% +% (n,f) \mid +% n \in \naturals \mid +% +% \forall n' \in \indexxset[\indexx[\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 \indexx[\indexx[\zeta](n)](n')) -% \land (f(x)= \zero) ) -% +% % 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) +% +% ( (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)$ +% 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)$ +% +% 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. @@ -726,7 +726,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % 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}$. +% 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]$. @@ -735,29 +735,29 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % % % -% 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$ +% 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} +% \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} +% \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]$. @@ -772,7 +772,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % %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}. @@ -784,13 +784,13 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % %Fix $x \in \dom{G}$. % %Then $x \in \carrier[X]$. % %\begin{byCase} -% % \caseOf{$x \in A$.} +% % \caseOf{$x \in A$.} % % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$. %% %% -% % \caseOf{$x \notin A$.} +% % \caseOf{$x \notin A$.} % % \begin{byCase} -% % \caseOf{$x \in B$.} +% % \caseOf{$x \in B$.} % % For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$. %% % % \caseOf{$x \notin B$.} @@ -802,7 +802,7 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % % % We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. -% \begin{subproof} +% \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}$. @@ -832,48 +832,48 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % %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](\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 +% % +% % 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 +% % 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} -% % -% % -% % - % - % - % - % - % +% % +% % +% % + % + % + % + % + % % We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$. % \begin{subproof} % Omitted. % \end{subproof} % $g$ is a staircase function and $\chain[g] = C$. % $g$ is a legal staircase function. - % - % - % We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ + % + % + % We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ % and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. % \begin{subproof} % Omitted. % \end{subproof} - % We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. + % We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. % \begin{subproof} % Omitted. % \end{subproof} @@ -891,28 +891,28 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. % Formalization idea of enumarted sequences: - % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} + % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} % - This should give all finite and infinte enumarable sequences % - Introduce a notion for the indexing of these enumarable sequences. % - Then we can define the limit of a enumarted sequence of functions. % --------------------------------------------------------- - % + % % Here we need a limit definition for sequences of functions % We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$ % \begin{subproof} % Omitted. % \end{subproof} - % + % % We show that $F(A) = 1$. % \begin{subproof} % Omitted. % \end{subproof} - % + % % We show that $F(B) = 0$. % \begin{subproof} % Omitted. - % \end{subproof} - % + % \end{subproof} + % % We show that $F$ is continuous. % \begin{subproof} % Omitted. @@ -920,5 +920,5 @@ This is the first attempt to prove Urysohns Lemma with the usage of struct. \end{proof} % %\begin{theorem}\label{urysohnone_safe} -% Contradiction. +% Contradiction. %\end{theorem} |