diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/set/filter.tex | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/library/set/filter.tex b/library/set/filter.tex index 59b647f..e196b64 100644 --- a/library/set/filter.tex +++ b/library/set/filter.tex @@ -51,12 +51,24 @@ Follows by \cref{filter_inter_in_iff}. \end{proof} +\begin{proposition}\label{filter_in_iff_exists_subset} + Let $F$ be a filter on $S$. + Suppose $B\subseteq S$. + Then $B\in F$ iff there exists $A\subseteq B$ such that $A\in F$. +\end{proposition} + + \subsection{Principal filters over a set} \begin{definition}\label{principalfilter} $\principalfilter{S}{A} = \{X\in\pow{S}\mid A\subseteq X\}$. \end{definition} +\begin{proposition}\label{principalfilter_iff} + Suppose $A, B\subseteq S$. + Then $B\in\principalfilter{S}{A}$ iff $A\subseteq B$. +\end{proposition} + \begin{proposition}\label{principalfilter_is_filter} Suppose $A\subseteq S$. Suppose $A$ is inhabited. |