From 342ac0ab2f01b0b98886a0b3db77917d86ded2dc Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 20:17:33 +0200
Subject: Add filter lemmas

---
 library/set/filter.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'library/set/filter.tex')

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.
-- 
cgit v1.2.3

