blob: e3730f34c5d196a8b6308fc0c105c2e9c4357151 (
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
|
\import{set.tex}
\import{set/bipartition.tex}
\import{topology/topological-space.tex}
\subsection{Disconnections}
\begin{definition}\label{disconnections}
$\disconnections{X} = \{ p\in\bipartitions{\carrier[X]} \mid \text{$\fst{p},\snd{p}\in\opens[X]$} \}$.
\end{definition}
\begin{abbreviation}\label{is_a_disconnection}
$D$ is a disconnection of $X$ iff $D\in\disconnections{X}$.
\end{abbreviation}
\begin{definition}\label{disconnected}
$X$ is disconnected iff there exist $U, V\in\opens[X]$
such that $\carrier[X]$ is partitioned by $U$ and $V$.
\end{definition}
\begin{proposition}\label{disconnection_from_disconnected}
Let $X$ be a topological space.
Suppose $X$ is disconnected.
Then there exists a disconnection of $X$.
\end{proposition}
\begin{proof}
Take $U, V\in\opens[X]$ such that $\carrier[X]$ is partitioned by $U$ and $V$
by \cref{disconnected}.
Then $(U, V)$ is a bipartition of $\carrier[X]$.
Thus $(U, V)$ is a disconnection of $X$ by \cref{disconnections,times_proj_elim,times_tuple_intro}.
\end{proof}
\begin{proposition}\label{disconnected_from_disconnection}
Let $X$ be a topological space.
Let $D$ be a disconnection of $X$.
Then $X$ is disconnected.
\end{proposition}
\begin{proof}
$\fst{D}, \snd{D}\in\opens[X]$.
$\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$.
\end{proof}
\begin{abbreviation}\label{connected}
$X$ is connected iff $X$ is not disconnected.
\end{abbreviation}
|
