From a5deeef9c3214f0f2ccd90789f5344a88544d65b Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 25 May 2024 01:21:17 +0200
Subject: Prove `emptyset_open` to replace structure axiom

---
 library/topology/topological-space.tex | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'library/topology/topological-space.tex')

diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index e467d48..2bbdf09 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -11,7 +11,6 @@
     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]$.
@@ -26,6 +25,15 @@
     $U$ is open in $X$ iff $U\in\opens[X]$.
 \end{abbreviation}
 
+\begin{proposition}\label{emptyset_open}
+    Let $X$ be a topological space.
+    Then $\emptyset$ is open in $X$.
+\end{proposition}
+\begin{proof}
+    We have $\unions{\emptyset} = \emptyset\subseteq\opens[X]$ by \cref{unions_emptyset,emptyset_subseteq}.
+    Follows by \cref{opens_unions}.
+\end{proof}
+
 \begin{proposition}\label{union_open}
     Let $X$ be a topological space.
     Suppose $A$, $B$ are open.
-- 
cgit v1.2.3