diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/topology/urysohn.tex | 43 | ||||
| -rw-r--r-- | library/topology/urysohn2.tex | 30 |
2 files changed, 53 insertions, 20 deletions
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex index b8a5fa5..79d65dc 100644 --- a/library/topology/urysohn.tex +++ b/library/topology/urysohn.tex @@ -100,6 +100,14 @@ The first tept will be a formalisation of chain constructions. \subsection{staircase function} +\begin{definition}\label{minimum} + $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$. +\end{definition} + +\begin{definition}\label{maximum} + $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$. +\end{definition} + \begin{definition}\label{intervalclosed} $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$. \end{definition} @@ -122,6 +130,9 @@ The first tept will be a formalisation of chain constructions. \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_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]} }$. \end{enumerate} \end{struct} @@ -311,13 +322,7 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{proof} -\begin{definition}\label{minimum} - $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$. -\end{definition} -\begin{definition}\label{maximum} - $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$. -\end{definition} \begin{proposition}\label{urysohnchain_induction_step_existence} Let $X$ be a urysohn space. @@ -562,6 +567,16 @@ The first tept will be a formalisation of chain constructions. Omitted. \end{subproof} + 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 + %\end{cases} +% + %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$. We show that for all $n \in \indexset[\zeta]$ we have $\index[\zeta](n)$ has cardinality $\pot(n)$. @@ -581,15 +596,19 @@ The first tept will be a formalisation of chain constructions. 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)$ + 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$. - % - % Follows by \cref{existence_of_staircase_function}. + 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} - Omitted. + \end{subproof} diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex index 40a3615..71de210 100644 --- a/library/topology/urysohn2.tex +++ b/library/topology/urysohn2.tex @@ -68,18 +68,32 @@ Let $H = \carrier[X] \setminus B$. Let $P = \{x \in \pow{X} \mid x = A \lor x = H \lor (x \in \pow{X} \land (\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{H}{X}))\}$. + Let $\eta = \carrier[X]$. - - - Define $f : X \to \reals$ such that $f(x) = $ + + % Provable + % vvv + Define $F : \eta \to \reals$ such that $F(x) =$ \begin{cases} - &(x + k) &\text{if} x \in X \land k \in \naturals - & x &\text{if} x \neq \zero - & \zero & \text{if} x = \zero - % & x ,x \in X <- will result in technicly ambigus parse + & \zero &\text{if} x \in A\\ + & \rfrac{1}{1+1} &\text{if} x \in (\carrier[X] \setminus (A \union B))\\ + & 1 &\text{if} x \in B \end{cases} - + %Define $f : \naturals \to \pow{P}$ such that $f(x)=$ + %\begin{cases} + % & \emptyset & \text{if} x = \zero \\ + % & \{A, H\} & \text{if} x = 1 \\ + % & G & \text{if} x \in (\naturals \setminus \{1, \zero\}) \land G = \{g \in \pow{P} \mid g \in f(n-1) \lor (g \notin f(n-1) \land g \in P) \} + %\end{cases} + + Let $D = \{d \mid d \in \rationals \mid \zero \leq d \leq 1\}$. + Take $R$ such that for all $q \in D$ we have for all $S \in P$ we have $q \mathrel{R} S$ iff + $q = \zero \land S = A$ or $q = 1 \land S = H$ or + for all $q_1, q_2, S_1, S_2$ + such that $q_1 \leq q \leq q_2$ and $q_1 \mathrel{R} S_1$ and $q_2 \mathrel{R} S_2$ + we have $\closure{S_1}{X} \subseteq \interior{S}{X} \subseteq \closure{S}{X} \subseteq \interior{S_2}{X}$ + and $q \mathrel{R} S$. Trivial. |