blob: 90c635dede33d7997b2723248cc79e45f2799013 (
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
|
\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$ such that $U,V\in\opens[X]$ and
$\carrier[X]$ is partitioned by $U$ and $V$
by \cref{disconnected}.
$(U,V)$ is a bipartition of $\carrier[X]$ by \cref{bipartition_intro}.
$\fst{(U,V)}=U$ by \cref{fst_eq}.
$\snd{(U,V)}=V$ by \cref{snd_eq}.
$(U,V)\in\disconnections{X}$ by \cref{disconnections}.
Follows by assumption.
\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}
$D\in\disconnections{X}$ by assumption.
$D\in\bipartitions{\carrier[X]}$ by \cref{disconnections}.
$\fst{D},\snd{D}\in\opens[X]$ by \cref{disconnections}.
$\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$
by \cref{bipartitions_of_a_set}.
Follows by \cref{disconnected}.
\end{proof}
\begin{abbreviation}\label{connected}
$X$ is connected iff $X$ is not disconnected.
\end{abbreviation}
|
