From 091da55df4de2d27697203fdddcdacd3c713b38c Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Thu, 23 May 2024 13:11:39 +0200
Subject: Update formatting

---
 library/set/powerset.tex | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'library/set/powerset.tex')

diff --git a/library/set/powerset.tex b/library/set/powerset.tex
index 80da4cb..7f30f68 100644
--- a/library/set/powerset.tex
+++ b/library/set/powerset.tex
@@ -6,8 +6,7 @@
     The powerset of $X$ denotes $\pow{X}$.
 \end{abbreviation}
 
-\begin{axiom}%
-\label{pow_iff}
+\begin{axiom}\label{pow_iff}
     $B\in\pow{A}$ iff $B\subseteq A$.
 \end{axiom}
 
@@ -76,7 +75,7 @@
 
 % LATER
 %\begin{proposition}\label{powerset_cons}
-%    Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
+%    $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$.
 %\end{proposition}
 
 \begin{proposition}\label{powerset_union_subseteq}
-- 
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/powerset.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