Merge pull request #2 from adelon/main

changes from main needs to be included

5 files changed, 98 insertions, 47 deletions

diff --git a/library/set.tex b/library/set.tex
index 33e5af4..2fd18ea 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,7 @@ The $\operatorname{\textsf{cons}}$ operation is determined by the following axio
     Follows by set extensionality.
 \end{proof}
 
-\begin{proposition}%
-\label{inter_subseteq}
-    $A\inter B\subseteq A$.
-\end{proposition}
-
-\begin{proposition}%
-\label{inter_emptyset}
+\begin{proposition}\label{inter_emptyset}
     $A\inter\emptyset = \emptyset$.
 \end{proposition}
 \begin{proof}
@@ -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/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..ec5866f 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}
 
@@ -47,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}
@@ -76,7 +86,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 6fc07d3..6fa9fbd 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}
@@ -75,32 +75,25 @@
 \end{proof}
 
 
-
-
 \begin{lemma}\label{inters_in_genopens}
     Assume $B$ is a topological basis for $X$.
-    Suppose $A, C\in \genOpens{B}{X}$.
-    
+    Assume $A, C\in \genOpens{B}{X}$.
     Then $(A\inter C) \in \genOpens{B}{X}$.
 \end{lemma}
 \begin{proof}
-    
-    Show $(A \inter C) \in \pow{X}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-    
+
+    We have $(A \inter C) \in \pow{X}$ by \cref{genopens,inter_powerset}.
+
 
     Show for all $x\in (A\inter C)$ there exists $W \in B$
     such that $x\in W$ and $W \subseteq (A\inter C)$.
     \begin{subproof}
         Fix $x \in (A\inter C)$.
-        $x \in A,C$.
-        There exist $V' \in B$ such that $x \in V'$ and $V' \subseteq A$ by \cref{genopens}. 
-        There exist $V'' \in B$ such that $x \in V''$ and $V'' \subseteq C$ by \cref{genopens}.
-        $x \in (V' \inter V'')$.
-        There exist $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$.
-        
+        Then $x\in A,C$.
+        There exists $V'  \in B$ such that $x \in V' \subseteq A$ by \cref{genopens}.
+        There exists $V'' \in B$ such that $x \in V''\subseteq C$ by \cref{genopens}.
+        There exists $W \in B$ such that $x \in W$ and $W \subseteq V'$ and $W \subseteq V''$.
+
         Show $W \subseteq (A\inter C)$.
         \begin{subproof}
             %$W \subseteq v'$ and $W \subseteq V''$.
@@ -111,11 +104,4 @@
     %such that $x\in W$ and $W \subseteq (A\inter C)$.
 
     $(A\inter C) \in \genOpens{B}{X}$.
-    
- 
 \end{proof}
-
-
-
-
-
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.