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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
\import{topology/topological-space.tex}
% T0 separation
\begin{definition}\label{is_kolmogorov}
$X$ is Kolmogorov iff
for all $x,y\in\carrier[X]$ such that $x\neq y$
there exist $U\in\opens[X]$ such that
$x\in U\not\ni y$ or $x\notin U\ni y$.
\end{definition}
\begin{abbreviation}\label{kolmogorov_space}
$X$ is a Kolmogorov space iff $X$ is a topological space and
$X$ is Kolmogorov.
\end{abbreviation}
\begin{abbreviation}\label{teezero}
$X$ is \teezero\ iff $X$ is Kolmogorov.
\end{abbreviation}
\begin{abbreviation}\label{teezero_space}
$X$ is a \teezero-space iff $X$ is a Kolmogorov space.
\end{abbreviation}
\begin{proposition}\label{kolmogorov_implies_kolmogorov_for_closeds}
Suppose $X$ is a Kolmogorov space.
Let $x,y\in\carrier[X]$.
Suppose $x\neq y$.
Then there exist $A\in\closeds{X}$ such that
$x\in A\not\ni y$ or $x\notin A\ni y$.
\end{proposition}
\begin{proof}
Take $U\in\opens[X]$ such that $x\in U\not\ni y$ or $x\notin U\ni y$
by \cref{is_kolmogorov}.
Then $\carrier[X]\setminus U\in\closeds{X}$ by \cref{complement_of_open_elem_closeds}.
Now $x\in (\carrier[X]\setminus U)\not\ni y$ or $x\notin (\carrier[X]\setminus U)\ni y$
by \cref{setminus}.
\end{proof}
\begin{proposition}\label{kolmogorov_for_closeds_implies_kolmogorov}
Suppose for all $x,y\in\carrier[X]$ such that $x\neq y$
there exist $U\in\closeds{X}$ such that
$x\in U\not\ni y$ or $x\notin U\ni y$.
Then $X$ is Kolmogorov.
\end{proposition}
\begin{proof}
Follows by \cref{closeds,is_closed_in,is_kolmogorov,setminus}.
\end{proof}
\begin{proposition}\label{kolmogorov_iff_kolmogorov_for_closeds}
Let $X$ be a topological space.
$X$ is Kolmogorov iff
for all $x,y\in\carrier[X]$ such that $x\neq y$
there exist $U\in\closeds{X}$ such that
$x\in U\not\ni y$ or $x\notin U\ni y$.
\end{proposition}
\begin{proof}
Follows by \cref{kolmogorov_implies_kolmogorov_for_closeds,kolmogorov_for_closeds_implies_kolmogorov}.
\end{proof}
% T1 separation (Fréchet topology)
\begin{definition}\label{teeone}
$X$ is \teeone\ iff
for all $x,y\in\carrier[X]$ such that $x\neq y$
there exist $U, V\in\opens[X]$ such that
$U\ni x\notin V$ and $V\ni y\notin U$.
\end{definition}
\begin{abbreviation}\label{teeone_space}
$X$ is a \teeone-space iff $X$ is a topological space and
$X$ is \teeone.
\end{abbreviation}
\begin{proposition}\label{teeone_implies_singletons_closed}
Let $X$ be a \teeone-space.
Then for all $x\in\carrier[X]$ we have $\{x\}$ is closed in $X$.
\end{proposition}
\begin{proof}
Omitted.
% TODO
% Choose for every y distinct from x and open subset U_y containing y but not x.
% The union U of all the U_y is open.
% {x} is the complement of U in \carrier[X].
\end{proof}
%
% Conversely, if \{x\} is open, then for any y distinct from x we can use
% X\setminus\{x\} as the open neighbourhood of y.
% T2 separation
\begin{definition}\label{is_hausdorff}
$X$ is Hausdorff iff
for all $x,y\in\carrier[X]$ such that $x\neq y$
there exist $U, V\in\opens[X]$ such that
$x\in U$ and $y\in V$ and $U$ is disjoint from $V$.
\end{definition}
\begin{abbreviation}\label{hausdorff_space}
$X$ is a Hausdorff space iff $X$ is a topological space and
$X$ is Hausdorff.
\end{abbreviation}
\begin{abbreviation}\label{teetwo}
$X$ is \teetwo\ iff $X$ is Hausdorff.
\end{abbreviation}
\begin{abbreviation}\label{teetwo_space}
$X$ is a \teetwo-space iff $X$ is a Hausdorff space.
\end{abbreviation}
\begin{proposition}\label{teeone_space_is_teezero_space}
Let $X$ be a \teeone-space.
Then $X$ is a \teezero-space.
\end{proposition}
\begin{proof}
Follows by \cref{is_kolmogorov,teeone}.
\end{proof}
\begin{proposition}\label{teetwo_space_is_teeone_space}
Let $X$ be a \teetwo-space.
Then $X$ is a \teeone-space.
\end{proposition}
\begin{proof}
Omitted. % TODO
\end{proof}
|
