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') 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') 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') 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') 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 From 091da55df4de2d27697203fdddcdacd3c713b38c Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Thu, 23 May 2024 13:11:39 +0200 Subject: Update formatting --- library/set/powerset.tex | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'library/set') diff --git a/library/set/powerset.tex b/library/set/powerset.tex index 80da4cb..7f30f68 100644 --- a/library/set/powerset.tex +++ b/library/set/powerset.tex @@ -6,8 +6,7 @@ The powerset of $X$ denotes $\pow{X}$. \end{abbreviation} -\begin{axiom}% -\label{pow_iff} +\begin{axiom}\label{pow_iff} $B\in\pow{A}$ iff $B\subseteq A$. \end{axiom} @@ -76,7 +75,7 @@ % LATER %\begin{proposition}\label{powerset_cons} -% Then $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$. +% $\pow{\cons{b}{A}} = \pow{A}\union \{\cons{b}{B}\mid B\in\pow{A}\}$. %\end{proposition} \begin{proposition}\label{powerset_union_subseteq} -- cgit v1.2.3 From 719bb860942fc1134ad4a4ae55db2713cd100f1a Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Tue, 28 May 2024 17:09:06 +0200 Subject: Pow closed under binary intersection --- library/set.tex | 13 +++++-------- library/set/powerset.tex | 11 +++++++++++ 2 files changed, 16 insertions(+), 8 deletions(-) (limited to 'library/set') diff --git a/library/set.tex b/library/set.tex index fcd2642..2fd18ea 100644 --- a/library/set.tex +++ b/library/set.tex @@ -551,14 +551,6 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio Follows by set extensionality. \end{proof} -\begin{proposition}\label{inter_subseteq_left} - $A\inter B\subseteq A$. -\end{proposition} - -\begin{proposition}\label{inter_subseteq_right} - $A\inter B\subseteq B$. -\end{proposition} - \begin{proposition}\label{inter_emptyset} $A\inter\emptyset = \emptyset$. \end{proposition} @@ -620,6 +612,11 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio Follows by set extensionality. \end{proof} +\begin{proposition}\label{inter_subseteq} + Suppose $A,B\subseteq C$. + Then $A\inter B\subseteq C$. +\end{proposition} + \begin{abbreviation}\label{closedunderinter} $T$ is closed under binary intersections iff for every $U,V\in T$ we have $U\inter V\in T$. diff --git a/library/set/powerset.tex b/library/set/powerset.tex index 7f30f68..ec5866f 100644 --- a/library/set/powerset.tex +++ b/library/set/powerset.tex @@ -46,6 +46,17 @@ Follows by \cref{pow_iff,unions_subseteq_of_powerset_is_subseteq}. \end{proof} + +\begin{proposition}\label{inter_powerset} + Let $A,B\in\pow{C}$. + Then $A\inter B\in\pow{C}$. +\end{proposition} +\begin{proof} + We have $A,B\subseteq C$ by \cref{pow_iff}. + $A\inter B\subseteq C$ by \cref{inter_subseteq}. + Follows by \cref{pow_iff}. +\end{proof} + \begin{proposition}\label{unions_powerset} $\unions{\pow{A}} = A$. \end{proposition} -- cgit v1.2.3