From 3845ab9020b3eb591ef999827503b483eb735bd7 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 21 May 2024 16:52:01 +0200
Subject: Add simple lemmas on filters

---
 library/set.tex | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'library/set.tex')

diff --git a/library/set.tex b/library/set.tex
index 33e5af4..e7e062f 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -553,13 +553,15 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}%
-\label{inter_subseteq}
+\begin{proposition}\label{inter_subseteq_left}
     $A\inter B\subseteq A$.
 \end{proposition}
 
-\begin{proposition}%
-\label{inter_emptyset}
+\begin{proposition}\label{inter_subseteq_right}
+    $A\inter B\subseteq B$.
+\end{proposition}
+
+\begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
 \begin{proof}
-- 
cgit v1.2.3


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/set.tex                        |  6 ++----
 library/topology/topological-space.tex | 10 +++++++++-
 2 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'library/set.tex')

diff --git a/library/set.tex b/library/set.tex
index e7e062f..fcd2642 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -131,8 +131,7 @@ which applies it to goals of the form “$A = B$” and  “$A \neq B$”.
     If $x$ and $y$ are empty, then $x = y$.
 \end{proposition}
 
-\begin{proposition}%
-\label{emptyset_subseteq}
+\begin{proposition}\label{emptyset_subseteq}
     For all $a$ we have $\emptyset \subseteq a$.
     % LATER $\emptyset$ is a subset of every set.
 \end{proposition}
@@ -266,8 +265,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     There exists $B\in C$ such that $A\in B$.
 \end{proof}
 
-\begin{proposition}%
-\label{unions_emptyset}
+\begin{proposition}\label{unions_emptyset}
     $\unions{\emptyset} = \emptyset$.
 \end{proposition}
 
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


From 719bb860942fc1134ad4a4ae55db2713cd100f1a Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 28 May 2024 17:09:06 +0200
Subject: Pow closed under binary intersection

---
 library/set.tex          | 13 +++++--------
 library/set/powerset.tex | 11 +++++++++++
 2 files changed, 16 insertions(+), 8 deletions(-)

(limited to 'library/set.tex')

diff --git a/library/set.tex b/library/set.tex
index fcd2642..2fd18ea 100644
--- a/library/set.tex
+++ b/library/set.tex
@@ -551,14 +551,6 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}\label{inter_subseteq_left}
-    $A\inter B\subseteq A$.
-\end{proposition}
-
-\begin{proposition}\label{inter_subseteq_right}
-    $A\inter B\subseteq B$.
-\end{proposition}
-
 \begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
@@ -620,6 +612,11 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
+\begin{proposition}\label{inter_subseteq}
+    Suppose $A,B\subseteq C$.
+    Then $A\inter B\subseteq C$.
+\end{proposition}
+
 \begin{abbreviation}\label{closedunderinter}
     $T$ is closed under binary intersections
     iff for every $U,V\in T$ we have $U\inter V\in T$.
diff --git a/library/set/powerset.tex b/library/set/powerset.tex
index 7f30f68..ec5866f 100644
--- a/library/set/powerset.tex
+++ b/library/set/powerset.tex
@@ -46,6 +46,17 @@
     Follows by \cref{pow_iff,unions_subseteq_of_powerset_is_subseteq}.
 \end{proof}
 
+
+\begin{proposition}\label{inter_powerset}
+    Let $A,B\in\pow{C}$.
+    Then $A\inter B\in\pow{C}$.
+\end{proposition}
+\begin{proof}
+    We have $A,B\subseteq C$ by \cref{pow_iff}.
+    $A\inter B\subseteq C$ by \cref{inter_subseteq}.
+    Follows by \cref{pow_iff}.
+\end{proof}
+
 \begin{proposition}\label{unions_powerset}
     $\unions{\pow{A}} = A$.
 \end{proposition}
-- 
cgit v1.2.3