blob: db46732298bd6d12af6b3d88c02c0019930c2385 (
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
|
\import{set.tex}
\import{set/cons.tex}
\import{set/powerset.tex}
\import{set/fixpoint.tex}
\import{set/product.tex}
\import{topology/topological-space.tex}
\import{topology/separation.tex}
\import{topology/continuous.tex}
\import{topology/basis.tex}
\import{numbers.tex}
\import{function.tex}
\section{The canonical topology on $\mathbbR$}
\begin{definition}\label{topological_basis_reals_eps_ball}
$\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
\end{definition}
\begin{axiom}\label{reals_carrier_reals}
$\carrier[\reals] = \reals$.
\end{axiom}
\begin{theorem}\label{topological_basis_reals_is_prebasis}
$\topoBasisReals$ is a topological prebasis for $\reals$.
\end{theorem}
\begin{proof}
We show that $\unions{\topoBasisReals} \subseteq \reals$.
\begin{subproof}
It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$.
Fix $x \in \unions{\topoBasisReals}$.
\end{subproof}
We show that $\reals \subseteq \unions{\topoBasisReals}$.
\begin{subproof}
It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
Fix $x \in \reals$.
\end{subproof}
\end{proof}
\begin{theorem}\label{topological_basis_reals_is_basis}
$\topoBasisReals$ is a topological basis for $\reals$.
\end{theorem}
\begin{proof}
$\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}.
Let $B = \topoBasisReals$.
It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
Fix $U \in B$.
Fix $V \in B$.
Fix $x \in U, V$.
\end{proof}
\begin{axiom}\label{topological_space_reals}
$\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
\end{axiom}
\begin{theorem}\label{reals_is_topological_space}
$\reals$ is a topological space.
\end{theorem}
\begin{proof}
$\topoBasisReals$ is a topological basis for $\reals$.
Let $B = \topoBasisReals$.
We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$.
\begin{subproof}
It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$.
Fix $A \in \opens[\reals]$.
Follows by \cref{powerset_elim,topological_space_reals,genopens}.
\end{subproof}
We show that $\reals \in\opens[\reals]$.
\begin{subproof}
$B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
$\unions{B} \in \genOpens{B}{\reals}$.
$\reals \subseteq \unions{B}$.
\end{subproof}
We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$.
\begin{subproof}
Follows by \cref{topological_space_reals,inters_in_genopens}.
\end{subproof}
We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$.
\begin{subproof}
Follows by \cref{topological_space_reals,union_in_genopens}.
\end{subproof}
$\carrier[\reals] = \reals$.
Follows by \cref{topological_space}.
\end{proof}
\begin{proposition}\label{open_interval_is_open}
Suppose $a,b \in \reals$.
Then $\intervalopen{a}{b} \in \opens[\reals]$.
\end{proposition}
|
