From 3845ab9020b3eb591ef999827503b483eb735bd7 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Tue, 21 May 2024 16:52:01 +0200
Subject: Add simple lemmas on filters

---
 library/set/filter.tex | 29 +++++++++++++++++++++++------
 1 file changed, 23 insertions(+), 6 deletions(-)

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

diff --git a/library/set/filter.tex b/library/set/filter.tex
index 2797d86..93309de 100644
--- a/library/set/filter.tex
+++ b/library/set/filter.tex
@@ -3,6 +3,8 @@
 
 \section{Filters}
 
+\subsection{Definition and basic properties of filters}
+
 \begin{abbreviation}\label{upwardclosed}
     $F$ is upward-closed in $S$ iff
     for all $A, B$ such that $A\subseteq B\subseteq S$ and $A\in F$ we have $B\in F$.
@@ -11,22 +13,37 @@
 \begin{definition}\label{filter}
     $F$ is a filter on $S$ iff
     $F$ is a family of subsets of $S$
-    and $S$ is inhabited
     and $S\in F$
     and $\emptyset\notin F$
     and $F$ is closed under binary intersections
     and $F$ is upward-closed in $S$.
 \end{definition}
 
+\begin{proposition}\label{filter_ext_complement}
+    Let $F, G$ be filters on $S$.
+    Suppose for all $A\subseteq S$ we have $S\setminus A\in F$ iff $S\setminus A\in G$.
+    Then $F = G$.
+\end{proposition}
+\begin{proof}
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{filter_inter_in_iff}
+    Let $F$ be a filter on $S$.
+    Suppose $A, B\subseteq S$.
+    Then $A\inter B\in F$ iff $A, B\in F$.
+\end{proposition}
+\begin{proof}
+    We have $A\inter B\subseteq A, B$.
+    Follows by \cref{filter}.
+\end{proof}
+
+\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_domain_inhabited}
-%    Suppose $F$ is a filter on $S$.
-%    Then $S$ is inhabited.
-%\end{proposition}
-
 \begin{proposition}\label{principalfilter_is_filter}
     Suppose $A\subseteq S$.
     Suppose $A$ is inhabited.
-- 
cgit v1.2.3


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(-)

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

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


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


From 9113b4fddb67e5a101e4a26ead3d1d1bf72664ce Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Wed, 22 May 2024 23:10:27 +0200
Subject: Update filter.tex

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

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

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