diff options
Diffstat (limited to 'library/set/filter.tex')
| -rw-r--r-- | library/set/filter.tex | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/library/set/filter.tex b/library/set/filter.tex index e196b64..4537b81 100644 --- a/library/set/filter.tex +++ b/library/set/filter.tex @@ -69,6 +69,16 @@ Then $B\in\principalfilter{S}{A}$ iff $A\subseteq B$. \end{proposition} +\begin{proposition}\label{principalfilter_bottom} + Suppose $A\subseteq S$. + Then $A\in\principalfilter{S}{A}$. +\end{proposition} + +\begin{proposition}\label{principalfilter_top} + Suppose $A\subseteq S$. + Then $S\in\principalfilter{S}{A}$. +\end{proposition} + \begin{proposition}\label{principalfilter_is_filter} Suppose $A\subseteq S$. Suppose $A$ is inhabited. |