blob: a64fa7ec4541fcd2712cf110a8e5c65f75f83405 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
\import{topology/topological-space.tex}
\import{topology/separation.tex}
\import{topology/continuous.tex}
\import{topology/basis.tex}
\import{numbers.tex}
\import{function.tex}
\import{set.tex}
\import{cardinal.tex}
\import{relation.tex}
\import{relation/uniqueness.tex}
\import{set/cons.tex}
\import{set/powerset.tex}
\import{set/fixpoint.tex}
\import{set/product.tex}
\section{Urysohns Lemma}
\begin{definition}\label{one_to_n_set}
$\seq{m}{n} = \{x \in \naturals \mid m \leq x \leq n\}$.
\end{definition}
\begin{struct}\label{sequence}
A sequence $X$ is a onesorted structure equipped with
\begin{enumerate}
\item $\index$
\item $\indexset$
\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]$.
\end{enumerate}
\end{struct}
\begin{abbreviation}\label{urysohnspace}
$X$ is a urysohn space iff
$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$.
\end{abbreviation}
\begin{definition}\label{intervalclosed}
$\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
\end{definition}
\begin{theorem}\label{urysohn}
Let $X$ be a urysohn space.
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}}$
and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
\end{theorem}
\begin{proof}
Define $f : X \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
\end{cases}
$U_1$
Trivial.
\end{proof}
\begin{theorem}\label{safe}
Contradiction.
\end{theorem}
|
