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/powerset.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

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

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