diff options
Diffstat (limited to 'library/set')
| -rw-r--r-- | library/set/powerset.tex | 11 |
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} |
