diff options
| -rw-r--r-- | library/set.tex | 13 | ||||
| -rw-r--r-- | library/set/powerset.tex | 11 |
2 files changed, 16 insertions, 8 deletions
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} |