blob: ea49a6cb57e075c3b9fb7bc5b7f15ac6b44b970e (
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
|
\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{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}
Trivial.
\end{proof}
\begin{theorem}\label{safe}
Contradiction.
\end{theorem}
|
