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
|
\import{topology/topological-space.tex}
\import{set.tex}
\import{set/powerset.tex}
\subsection{Topological basis}
\begin{abbreviation}\label{covers}
$C$ covers $X$ iff
for all $x\in X$ there exists $U\in C$ such that $x\in U$.
\end{abbreviation}
\begin{proposition}\label{covers_unions_intro}
Suppose $C$ covers $X$.
Then $X\subseteq\unions{C}$.
\end{proposition}
\begin{proposition}\label{covers_unions_elim}
Suppose $X\subseteq\unions{C}$.
Then $C$ covers $X$.
\end{proposition}
% Also called "prebase", "subbasis", or "subbase". We prefer "pre-" or "quasi-"
% for consistency when handling generalizations, even if "subbasis" is more common.
\begin{abbreviation}\label{topological_prebasis}
$B$ is a topological prebasis for $X$ iff $\unions{B} = X$.
\end{abbreviation}
\begin{proposition}\label{topological_prebasis_iff_covering_family}
$B$ is a topological prebasis for $X$ iff
$B$ is a family of subsets of $X$ and $B$ covers $X$.
\end{proposition}
\begin{proof}
If $B$ is a family of subsets of $X$ and $B$ covers $X$,
then $\unions{B} = X$
by \cref{subseteq_antisymmetric,unions_family,covers_unions_intro}.
If $\unions{B} = X$,
then $B$ is a family of subsets of $X$ and $B$ covers $X$
by \cref{covers_unions_intro,subseteq_refl,covers_unions_elim}.
\end{proof}
% Also called "base of topology".
\begin{definition}\label{topological_basis}
$B$ is a topological basis for $X$ iff
$B$ is a topological prebasis for $X$ and
for all $U, V, x$ such that $U, V\in B$ and $x\in U,V$
there exists $W\in B$ such that $x\in W\subseteq U, V$.
\end{definition}
\begin{definition}\label{genopens}
$\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$
\\ such that $x\in V\subseteq U$}\right\}$.
\end{definition}
\begin{lemma}\label{emptyset_in_genopens}
Assume $B$ is a topological basis for $X$.
$\emptyset \in \genOpens{B}{X}$.
\end{lemma}
\begin{lemma}\label{all_is_in_genopens}
Assume $B$ is a topological basis for $X$.
$X \in \genOpens{B}{X}$.
\end{lemma}
\begin{proof}
$B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
$\unions{B} \in \genOpens{B}{X}$.
$X \subseteq \unions{B}$.
\end{proof}
\begin{lemma}\label{union_in_genopens}
Assume $B$ is a topological basis for $X$.
For all $F\subseteq \genOpens{B}{X}$ we have $\unions{F}\in\genOpens{B}{X}$.
\end{lemma}
\begin{proof}
Omitted.
\end{proof}
\begin{lemma}\label{inters_in_genopens}
Assume $B$ is a topological basis for $X$.
%For all $A, C$
If $A\in \genOpens{B}{X}$ and $C\in \genOpens{B}{X}$ then $(A\inter C) \in \genOpens{B}{X}$.
\end{lemma}
\begin{proof}
Show $(A \inter C) \in \pow{X}$.
\begin{subproof}
$(A \inter C) \subseteq X$ by assumption.
\end{subproof}
Therefore for all $A, C \in \genOpens{B}{X}$ we have $(A \inter C) \in \pow{X}$.
Show for all $x\in (A\inter C)$ there exists $W \in B$
such that $x\in W$ and $W \subseteq (A\inter C)$.
\begin{subproof}
Fix $x \in (A\inter C)$.
There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by assumption. %TODO: Warum muss hier by assumtion hin?
There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by assumption.
There exist $W \in B$ such that $x \in W$ and $W \subseteq v'$ and $W \subseteq V''$ by assumption.
Show $W \subseteq (A\inter C)$.
\begin{subproof}
%$W \subseteq v'$ and $W \subseteq V''$.
For all $y \in W$ we have $y \in V'$ and $y \in V''$ by assumption.
\end{subproof}
\end{subproof}
%Therefore for all $A, C, x$ such that $A \in \genOpens{B}{X}$ and $C \in \genOpens{B}{X}$ and $x \in (A \inter C)$ we have there exists $W \in B$
%such that $x\in W$ and $W \subseteq (A\inter C)$.
$(A\inter C) \in \genOpens{B}{X}$ by assumption.
\end{proof}
|
