diff options
| -rw-r--r-- | library/topology/urysohn.tex | 44 |
1 files changed, 40 insertions, 4 deletions
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index 6662706..0c4052d 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -410,7 +410,7 @@ The first tept will be a formalisation of chain constructions. Suppose $A,B \in \closeds{X}$. Suppose $A \inter B$ is empty. There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ - and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous. + and $f(A) = 0$ and $f(B)= 1$ and $f$ is continuous. \end{theorem} \begin{proof} @@ -442,8 +442,10 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} - For all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. - + We show that for all $m \in \indexset[\zeta]$ we have $\pot(m) \neq \zero$. + \begin{subproof} + Omitted. + \end{subproof} %%------------- Maybe use Abstrect.hs line 368 "Local Function". @@ -495,9 +497,43 @@ The first tept will be a formalisation of chain constructions. \}$. + Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$. + + + We show that there exist $F$ such that + $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and + for all $x \in \carrier[X]$ we have + there exist $k \in \intervalclosed{\zero}{1}$ + such that $F(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{(k - \apply{\gamma(N')}{x})} \leq \epsilon$. + \begin{subproof} + Omitted. + \end{subproof} + - + We show that $F \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that $F(A) = 0$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that $F(B) = 1$. + \begin{subproof} + Omitted. + \end{subproof} + + We show that $F$ is continuous. + \begin{subproof} + Omitted. + \end{subproof} %Suppose $\eta$ is a urysohnchain in $X$. %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$ |