blob: 71de21004f89e05641cf04651c62cca09acf2ced (
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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
|
\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{urysohnsetinbeetween}
Let $X$ be a urysohn space.
Suppose $A,B \in \closeds{X}$.
Suppose $\closure{A}{X} \subseteq \interior{B}{X}$.
Suppose $\carrier[X]$ is inhabited.
There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$.
\end{theorem}
\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}
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]$.
% Provable
% vvv
Define $F : \eta \to \reals$ such that $F(x) =$
\begin{cases}
& \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.
\end{proof}
\begin{theorem}\label{safe}
Contradiction.
\end{theorem}
|
