diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/set.tex | 16 | ||||
| -rw-r--r-- | library/set/filter.tex | 64 | ||||
| -rw-r--r-- | library/set/powerset.tex | 5 | ||||
| -rw-r--r-- | library/topology/basis.tex | 4 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 10 |
5 files changed, 78 insertions, 21 deletions
diff --git a/library/set.tex b/library/set.tex index 33e5af4..fcd2642 100644 --- a/library/set.tex +++ b/library/set.tex @@ -131,8 +131,7 @@ which applies it to goals of the form “$A = B$” and “$A \neq B$”. If $x$ and $y$ are empty, then $x = y$. \end{proposition} -\begin{proposition}% -\label{emptyset_subseteq} +\begin{proposition}\label{emptyset_subseteq} For all $a$ we have $\emptyset \subseteq a$. % LATER $\emptyset$ is a subset of every set. \end{proposition} @@ -266,8 +265,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio There exists $B\in C$ such that $A\in B$. \end{proof} -\begin{proposition}% -\label{unions_emptyset} +\begin{proposition}\label{unions_emptyset} $\unions{\emptyset} = \emptyset$. \end{proposition} @@ -553,13 +551,15 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio Follows by set extensionality. \end{proof} -\begin{proposition}% -\label{inter_subseteq} +\begin{proposition}\label{inter_subseteq_left} $A\inter B\subseteq A$. \end{proposition} -\begin{proposition}% -\label{inter_emptyset} +\begin{proposition}\label{inter_subseteq_right} + $A\inter B\subseteq B$. +\end{proposition} + +\begin{proposition}\label{inter_emptyset} $A\inter\emptyset = \emptyset$. \end{proposition} \begin{proof} diff --git a/library/set/filter.tex b/library/set/filter.tex index 2797d86..4537b81 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,21 +13,71 @@ \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} + +\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} + +\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_domain_inhabited} -% Suppose $F$ is a filter on $S$. -% Then $S$ is inhabited. -%\end{proposition} +\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_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$. @@ -55,8 +107,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 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} diff --git a/library/topology/basis.tex b/library/topology/basis.tex index 61a358f..15910f9 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -47,8 +47,8 @@ \end{definition} \begin{definition}\label{genopens} - $\genOpens{B}{X} = \{ U\in\pow{X} \mid \text{for all $x\in U$ there exists $V\in B$ - such that $x\in V\subseteq U$} \}$. + $\genOpens{B}{X} = \left\{ U\in\pow{X} \middle| \textbox{for all $x\in U$ there exists $V\in B$ + \\ such that $x\in V\subseteq U$}\right\}$. \end{definition} \begin{lemma}\label{emptyset_in_genopens} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index e467d48..2bbdf09 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -11,7 +11,6 @@ such that \begin{enumerate} \item\label{opens_type} $\opens[X]$ is a family of subsets of $\carrier[X]$. - \item\label{emptyset_open} $\emptyset\in\opens[X]$. \item\label{carrier_open} $\carrier[X]\in\opens[X]$. \item\label{opens_inter} For all $A, B\in \opens[X]$ we have $A\inter B\in\opens[X]$. \item\label{opens_unions} For all $F\subseteq \opens[X]$ we have $\unions{F}\in\opens[X]$. @@ -26,6 +25,15 @@ $U$ is open in $X$ iff $U\in\opens[X]$. \end{abbreviation} +\begin{proposition}\label{emptyset_open} + Let $X$ be a topological space. + Then $\emptyset$ is open in $X$. +\end{proposition} +\begin{proof} + We have $\unions{\emptyset} = \emptyset\subseteq\opens[X]$ by \cref{unions_emptyset,emptyset_subseteq}. + Follows by \cref{opens_unions}. +\end{proof} + \begin{proposition}\label{union_open} Let $X$ be a topological space. Suppose $A$, $B$ are open. |