From 3e4e7afc69bf43b3b45bde346c92f267e9b15c39 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 16:58:06 +0200
Subject: Add lemma `filter_setminus_in`

---
 library/set/filter.tex | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

diff --git a/library/set/filter.tex b/library/set/filter.tex
index 93309de..59b647f 100644
--- a/library/set/filter.tex
+++ b/library/set/filter.tex
@@ -38,6 +38,19 @@
     Follows by \cref{filter}.
 \end{proof}
 
+\begin{proposition}\label{filter_setminus_in}
+    Let $F$ be a filter on $S$.
+    Suppose $A\in F$.
+    Suppose $B\subseteq S$ and $S\setminus B\in F$.
+    Then $A\setminus B\in F$.
+\end{proposition}
+\begin{proof}
+    We have $A\subseteq S$.
+    Thus $A\setminus B = A\inter (S\setminus B)$ by \cref{setminus_eq_inter_complement}.
+    Now $S\setminus B\subseteq S$.
+    Follows by \cref{filter_inter_in_iff}.
+\end{proof}
+
 \subsection{Principal filters over a set}
 
 \begin{definition}\label{principalfilter}
@@ -72,8 +85,6 @@
     Suppose $X\notin\principalfilter{S}{A}$.
     Then $A\not\subseteq X$.
 \end{proposition}
-\begin{proof}
-\end{proof}
 
 \begin{definition}\label{maximalfilter}
     $F$ is a maximal filter on $S$ iff
-- 
cgit v1.2.3