summaryrefslogtreecommitdiff
path: root/library/set
diff options
context:
space:
mode:
Diffstat (limited to 'library/set')
-rw-r--r--library/set/powerset.tex11
1 files changed, 11 insertions, 0 deletions
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}