From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 10 Feb 2024 02:22:14 +0100
Subject: Initial commit

---
 library/topology/basis.tex             |  45 ++++++
 library/topology/disconnection.tex     |  44 ++++++
 library/topology/preclosure.tex        |  18 +++
 library/topology/separation.tex        | 124 ++++++++++++++++
 library/topology/topological-space.tex | 258 +++++++++++++++++++++++++++++++++
 5 files changed, 489 insertions(+)
 create mode 100644 library/topology/basis.tex
 create mode 100644 library/topology/disconnection.tex
 create mode 100644 library/topology/preclosure.tex
 create mode 100644 library/topology/separation.tex
 create mode 100644 library/topology/topological-space.tex

(limited to 'library/topology')

diff --git a/library/topology/basis.tex b/library/topology/basis.tex
new file mode 100644
index 0000000..dda187c
--- /dev/null
+++ b/library/topology/basis.tex
@@ -0,0 +1,45 @@
+\import{topology/topological-space.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}
diff --git a/library/topology/disconnection.tex b/library/topology/disconnection.tex
new file mode 100644
index 0000000..e3730f3
--- /dev/null
+++ b/library/topology/disconnection.tex
@@ -0,0 +1,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}
diff --git a/library/topology/preclosure.tex b/library/topology/preclosure.tex
new file mode 100644
index 0000000..6c104be
--- /dev/null
+++ b/library/topology/preclosure.tex
@@ -0,0 +1,18 @@
+\import{set.tex}
+
+\section{Preclosure spaces}
+
+
+\begin{struct}
+    A preclosure space $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\cl$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item For all $Y\subseteq X$ we have $\cl(Y)\subseteq X$.
+        \item $\cl(\emptyset) = \emptyset$.
+        \item For all $A$ we have $A\subseteq \cl(A)$.
+        \item For all $A, B$ we have $\cl(A\union B) = \cl(A) \union \cl(B)$.
+    \end{enumerate}
+\end{struct}
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
new file mode 100644
index 0000000..f70cb50
--- /dev/null
+++ b/library/topology/separation.tex
@@ -0,0 +1,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}
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
new file mode 100644
index 0000000..e467d48
--- /dev/null
+++ b/library/topology/topological-space.tex
@@ -0,0 +1,258 @@
+\import{set.tex}
+\import{set/powerset.tex}
+
+\section{Topological spaces}
+
+\begin{struct}\label{topological_space}
+    A topological space $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\opens$
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \item\label{opens_type} $\opens[X]$ is a family of subsets of $\carrier[X]$.
+        \item\label{emptyset_open} $\emptyset\in\opens[X]$.
+        \item\label{carrier_open} $\carrier[X]\in\opens[X]$.
+        \item\label{opens_inter} For all $A, B\in \opens[X]$ we have $A\inter B\in\opens[X]$.
+        \item\label{opens_unions} For all $F\subseteq \opens[X]$ we have $\unions{F}\in\opens[X]$.
+    \end{enumerate}
+\end{struct}
+
+\begin{abbreviation}\label{is_open_in}
+    $U$ is open iff $U\in\opens$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{is_open}
+    $U$ is open in $X$ iff $U\in\opens[X]$.
+\end{abbreviation}
+
+\begin{proposition}\label{union_open}
+    Let $X$ be a topological space.
+    Suppose $A$, $B$ are open.
+    Then $A\union B$ is open.
+\end{proposition}
+\begin{proof}
+    $\{A, B\}\subseteq \opens$.
+    $\unions{\{A, B\}}$ is open.
+    $\unions{\{A, B\}} = A\union B$.
+\end{proof}
+
+\begin{definition}[Interiors]\label{interiors}
+    $\interiors{A}{X} = \{ U\in\opens[X]\mid U\subseteq A\}$.
+\end{definition}
+
+\begin{definition}[Interior]\label{interior}
+    $\interior{A}{X} = \unions{\interiors{A}{X}}$.
+\end{definition}
+
+\begin{proposition}[Interior]\label{interior_elem_intro}
+    Suppose $U\in\opens[X]$ and $a\in U\subseteq A$.
+    Then $a\in\interior{A}{X}$.
+\end{proposition}
+\begin{proof}
+    $U\in\interiors{A}{X}$.
+\end{proof}
+
+\begin{proposition}[Interior]\label{interior_elem_elim}
+    Suppose $a\in\interior{A}{X}$.
+    Then there exists $U\in\opens[X]$
+    such that $a\in U\subseteq A$.
+\end{proposition}
+\begin{proof}
+    Take $U\in\interiors{A}{X}$ such that $a\in U$.
+\end{proof}
+
+\begin{proposition}[Interior]\label{interior_elem_iff}
+    $a\in\interior{A}{X}$ iff
+    there exists $U\in\opens[X]$
+    such that $a\in U\subseteq A$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{interior_elem_intro,interior_elem_elim}.
+\end{proof}
+
+\begin{proposition}\label{interior_of_open}
+    Let $X$ be a topological space.
+    Suppose $U$ is open in $X$.
+    Then $\interior{U}{X} = U$.
+\end{proposition}
+\begin{proof}
+    $U\in\interiors{U}{X}$.
+    Follows by \cref{subseteq,interior_elem_iff,neq_witness}.
+\end{proof}
+
+\begin{proposition}\label{interior_is_open}
+    Let $X$ be a topological space.
+    Then $\interior{A}{X}$ is open.
+\end{proposition}
+\begin{proof}
+    $\interiors{A}{X}\subseteq\opens[X]$.
+\end{proof}
+
+\begin{proposition}\label{interior_subseteq}
+    Then $\interior{A}{X}\subseteq A$.
+\end{proposition}
+
+\begin{proposition}\label{interior_maximal}
+    Let $X$ be a topological space.
+    Suppose $U\subseteq A\subseteq \carrier[X]$.
+    Suppose $U$ is open.
+    Then $U\subseteq \interior{A}{X}$.
+\end{proposition}
+
+\begin{proposition}\label{interior_eq_self_implies_open}
+    Let $X$ be a topological space.
+    Suppose $\interior{A}{X} = A$.
+    Then $A$ is open.
+\end{proposition}
+
+\begin{corollary}\label{interior_eq_self_iff_open}
+    Let $X$ be a topological space.
+    Then $\interior{A}{X} = A$ iff $A$ is open in $X$.
+\end{corollary}
+
+\begin{proposition}\label{interior_carrier}
+    Let $X$ be a topological space.
+    $\interior{\carrier[X]}{X} = \carrier[X]$.
+\end{proposition}
+\begin{proof}
+    $\carrier[X]\in\opens[X]$.
+    $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}.
+    Thus $\carrier[X]\in\interiors{\carrier[X]}{X}$ by \cref{interiors}.
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{interior_type}
+    Let $X$ be a topological space.
+    Then $\interior{A}{X}\in\pow{\carrier[X]}$.
+\end{proposition}
+\begin{proof}
+    We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$.
+    % As they are open subsets of X containing A
+    %
+    Thus $\interior{A}{X}\subseteq \carrier[X]$ by \cref{interior,unions_subseteq_of_powerset_is_subseteq}.
+\end{proof}
+
+\subsection{Closed sets}
+
+\begin{definition}\label{is_closed_in}
+    $A$ is closed in $X$ iff $\carrier[X]\setminus A$ is open in $X$.
+\end{definition}
+
+\begin{abbreviation}\label{is_clopen_in}
+    $A$ is clopen in $X$ iff $A$ is open in $X$ and closed in $X$.
+\end{abbreviation}
+
+\begin{proposition}\label{emptyset_is_closed}
+    Let $X$ be a topological space.
+    Then $\emptyset$ is closed in $X$.
+\end{proposition}
+\begin{proof}
+    $\carrier[X]\setminus \emptyset = \carrier[X]$.
+\end{proof}
+
+\begin{proposition}\label{carrier_is_closed}
+    Let $X$ be a topological space.
+    Then $\emptyset$ is closed in $X$.
+\end{proposition}
+\begin{proof}
+    $\carrier[X]\setminus \carrier[X] = \emptyset$.
+\end{proof}
+
+\begin{definition}[Closed sets]\label{closeds}
+    $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$.
+\end{definition}
+
+\begin{proposition}\label{complement_of_open_elem_closeds}
+    Let $X$ be a topological space.
+    Let $U\in\opens[X]$.
+    Then $\carrier[X]\setminus U\in\closeds{X}$.
+\end{proposition}
+\begin{proof}
+    $\carrier[X]\setminus U\in\pow{\carrier[X]}$.
+    $U\subseteq\carrier[X]$ by \cref{opens_type}.
+    Hence $\carrier[X]\setminus(\carrier[X]\setminus U) = U$ by \cref{double_relative_complement}.
+    $\carrier[X]\setminus U$ is closed in $X$.
+\end{proof}
+
+
+\begin{definition}[Closed covers]\label{closures}
+    $\closures{A}{X} = \{ D\in\pow{\carrier[X]}\mid \text{$A\subseteq D$ and $D$ is closed in $X$}\}$.
+\end{definition}
+
+\begin{definition}[Closure]\label{closure}
+    $\closure{A}{X} = \inters{\closures{A}{X}}$.
+\end{definition}
+
+\begin{proposition}\label{closure_emptyset}
+    Let $X$ be a topological space.
+    Then $\closure{\emptyset}{X} = \emptyset$.
+\end{proposition}
+\begin{proof}
+    $\emptyset\in\closures{\emptyset}{X}$.
+\end{proof}
+
+\begin{proposition}\label{closure_carrier}
+    Let $X$ be a topological space.
+    Then $\closure{\carrier[X]}{X} = \carrier[X]$.
+\end{proposition}
+\begin{proof}
+    %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$ by \cref{closures}.
+    %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\supseteq D$ by \cref{pow_iff,closures}.
+    %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ by \cref{subseteq_antisymmetric}.
+    For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$
+        by \cref{pow_iff,closures,subseteq_antisymmetric}.
+    Now $\carrier[X]\in\closures{\carrier[X]}{X}$.
+    Thus $\closures{\carrier[X]}{X} = \{\carrier[X]\}$
+        by \cref{singleton_iff_inhabited_subsingleton}.
+    Follows by \cref{inters_singleton,closure}.
+\end{proof}
+
+
+\begin{proposition}%[Complement of interior equals closure of complement]
+\label{complement_interior_eq_closure_complement}
+    $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$.
+\end{proposition}
+\begin{proof}
+    Omitted. % Use general De Morgan's Law in Pow|X|
+\end{proof}
+
+\begin{definition}[Frontier]\label{frontier}
+    $\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$.
+\end{definition}
+
+
+
+\begin{proposition}%[Frontier as intersection of closures]
+\label{frontier_as_inter}
+    $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$.
+\end{proposition}
+\begin{proof}
+    % TODO
+    Omitted.
+    %$\frontier{A}{X} = \closure{A}{X}\setminus\interior{A}{X}$. % by frontier (definition)
+    %$\closure{A}{X}\setminus\interior{A}{X} = \closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$. % by setminus_eq_inter_complement
+    %$\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. % by complement_interior_eq_closure_complement
+\end{proof}
+
+\begin{proposition}\label{frontier_of_emptyset}
+    Let $X$ be a topological space.
+    Then $\frontier{\emptyset}{X} = \emptyset$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{frontier_of_carrier}
+    Let $X$ be a topological space.
+    Then $\frontier{\carrier[X]}{X} = \emptyset$.
+\end{proposition}
+\begin{proof}
+    $\frontier{\carrier[X]}{X} = \carrier[X]\setminus\carrier[X]$
+        by \cref{frontier,interior_carrier,closure_carrier}.
+    Follows by \cref{setminus_self}.
+\end{proof}
+
+\begin{definition}\label{neighbourhoods}
+    $\neighbourhoods{x}{X} = \{U\in\opens[X] \mid x\in U\}$.
+\end{definition}
-- 
cgit v1.2.3