diff options
Diffstat (limited to 'library/topology')
| -rw-r--r-- | library/topology/basis.tex | 105 | ||||
| -rw-r--r-- | library/topology/disconnection.tex | 18 | ||||
| -rw-r--r-- | library/topology/preclosure.tex | 14 | ||||
| -rw-r--r-- | library/topology/separation.tex | 23 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 375 |
5 files changed, 347 insertions, 188 deletions
diff --git a/library/topology/basis.tex b/library/topology/basis.tex index cc9d7e5..4c1ac79 100644 --- a/library/topology/basis.tex +++ b/library/topology/basis.tex @@ -13,11 +13,23 @@ Suppose $C$ covers $X$. Then $X\subseteq\unions{C}$. \end{proposition} +\begin{proof} + For all $x\in X$ there exists $U\in C$ such that $x\in U$ + by assumption. + For all $x\in X$ we have $x\in\unions{C}$ by \cref{unions_iff}. + Follows by \cref{subseteq}. +\end{proof} \begin{proposition}\label{covers_unions_elim} Suppose $X\subseteq\unions{C}$. Then $C$ covers $X$. \end{proposition} +\begin{proof} + For all $x\in X$ we have $x\in\unions{C}$ by \cref{subseteq}. + For all $x\in X$ there exists $U\in C$ such that $x\in U$ + by \cref{unions_iff}. + Follows by assumption. +\end{proof} % Also called "prebase", "subbasis", or "subbase". We prefer "pre-" or "quasi-" % for consistency when handling generalizations, even if "subbasis" is more common. @@ -36,6 +48,7 @@ If $\unions{B} = X$, then $B$ is a family of subsets of $X$ and $B$ covers $X$ by \cref{covers_unions_intro,subseteq_refl,covers_unions_elim}. + Follows by assumption. \end{proof} % Also called "base of topology". @@ -55,6 +68,13 @@ Assume $B$ is a topological basis for $X$. $\emptyset \in \genOpens{B}{X}$. \end{lemma} +\begin{proof} + $\emptyset\in\pow{X}$ by \cref{emptyset_subseteq,pow_iff}. + For all $x\in\emptyset$ there exists $V\in B$ + such that $x\in V\subseteq\emptyset$ + by \cref{emptyset_subseteq,subseteq}. + Follows by \cref{genopens}. +\end{proof} @@ -64,18 +84,25 @@ Then $\unions{F}\in\genOpens{B}{X}$. \end{lemma} \begin{proof} - We have $\unions{F} \in \pow{X}$ by \cref{genopens,subseteq,pow_iff,unions_family,powerset_elim}. + For all $x\in\unions{F}$ we have $x\in X$ + by \cref{unions_iff,genopens,subseteq}. + We have $\unions{F}\in\pow{X}$ by \cref{pow_iff,subseteq}. - Show for all $x\in \unions{F}$ there exists $W \in B$ - such that $x\in W$ and $W \subseteq \unions{F}$. + Show for all $x$ we have if $x\in\unions{F}$, then + there exists $W\in B$ such that $x\in W$ and + $W\subseteq\unions{F}$. \begin{subproof} - Fix $x \in \unions{F}$. - There exists $V \in F$ such that $x \in V$ by \cref{unions_iff}. - $V \in \genOpens{B}{X}$. - There exists $W \in B$ such that $x \in W \subseteq V$. - Then $W \subseteq \unions{F}$. + Fix $x$. + Assume $x\in\unions{F}$. + Take $V$ such that $V\in F$ and $x\in V$ by \cref{unions_iff}. + $V\in\genOpens{B}{X}$ by \cref{subseteq}. + Take $W$ such that $W\in B$ and $x\in W\subseteq V$ + by \cref{genopens}. + $V\subseteq\unions{F}$ by \cref{unions_iff,subseteq}. + $W\subseteq\unions{F}$ by \cref{subseteq_transitive}. + Follows by assumption. \end{subproof} - Then $\unions{F}\in\genOpens{B}{X}$ by \cref{genopens}. + Follows by \cref{genopens}. \end{proof} \begin{lemma}\label{basis_is_in_genopens} @@ -83,14 +110,19 @@ $B \subseteq \genOpens{B}{X}$. \end{lemma} \begin{proof} - We show for all $V \in B$ $V \in \genOpens{B}{X}$. + Show for all $V$ we have if $V\in B$, then + $V\in\genOpens{B}{X}$. \begin{subproof} - Fix $V \in B$. - For all $x \in V$ $x \in V \subseteq V$. - $V \subseteq X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. - $V \in \pow{X}$. - $V \in \genOpens{B}{X}$. + Fix $V$. + Assume $V\in B$. + $V\subseteq X$ + by \cref{topological_prebasis_iff_covering_family,topological_basis}. + $V\in\pow{X}$ by \cref{pow_iff,subseteq}. + For all $x\in V$ there exists $W\in B$ + such that $x\in W\subseteq V$ by \cref{subseteq_refl}. + Follows by \cref{genopens}. \end{subproof} + Follows by \cref{subseteq}. \end{proof} \begin{lemma}\label{all_is_in_genopens} @@ -98,11 +130,10 @@ $X \in \genOpens{B}{X}$. \end{lemma} \begin{proof} - $B$ covers $X$ by \cref{topological_prebasis_iff_covering_family,topological_basis}. - $\unions{B} \in \genOpens{B}{X}$. - $X \subseteq \unions{B}$. - For all $x\in X$ there exists $V\in B$ such that $x\in V\subseteq X$. - Follows by \cref{powerset_top,genopens}. + $X\in\pow{X}$ by \cref{pow_iff,subseteq_refl}. + For all $x\in X$ there exists $V\in B$ such that $x\in V\subseteq X$ + by \cref{topological_prebasis_iff_covering_family,topological_basis,pow_iff,subseteq}. + Follows by \cref{genopens}. \end{proof} \begin{lemma}\label{inters_in_genopens} @@ -111,23 +142,25 @@ Then $(A\inter C) \in \genOpens{B}{X}$. \end{lemma} \begin{proof} + For all $x\in A\inter C$ we have $x\in X$ + by \cref{genopens,inter_elim_left,pow_iff,subseteq}. + We have $(A\inter C)\in\pow{X}$ by \cref{pow_iff,subseteq}. - 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$. + Show for all $x$ we have if $x\in A\inter C$, then + there exists $W\in B$ such that $x\in W$ and $W\subseteq A\inter C$. \begin{subproof} - Fix $x \in A\inter C$. - 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 \subseteq V', V''$ by \cref{topological_basis}. - - Show $W \subseteq A\inter C$. - \begin{subproof} - For all $y \in W$ we have $y \in V'$ and $y \in V''$. - \end{subproof} + Fix $x$. + Assume $x\in A\inter C$. + $x\in A,C$ by \cref{inter_elim_left,inter_elim_right}. + Take $V'$ such that $V'\in B$ and $x\in V'\subseteq A$ + by \cref{genopens}. + Take $V''$ such that $V''\in B$ and $x\in V''\subseteq C$ + by \cref{genopens}. + Take $W$ such that $W\in B$ and $x\in W$ and + $W\subseteq V',V''$ by \cref{topological_basis}. + $W\subseteq A,C$ by \cref{subseteq_transitive}. + $W\subseteq A\inter C$ by \cref{inter_intro,subseteq}. + Follows by assumption. \end{subproof} - - $(A\inter C) \in \genOpens{B}{X}$ by \cref{genopens}. + Follows by \cref{genopens}. \end{proof} diff --git a/library/topology/disconnection.tex b/library/topology/disconnection.tex index e3730f3..90c635d 100644 --- a/library/topology/disconnection.tex +++ b/library/topology/disconnection.tex @@ -23,10 +23,14 @@ Then there exists a disconnection of $X$. \end{proposition} \begin{proof} - Take $U, V\in\opens[X]$ such that $\carrier[X]$ is partitioned by $U$ and $V$ + Take $U,V$ such that $U,V\in\opens[X]$ and + $\carrier[X]$ is partitioned by $U$ and $V$ by \cref{disconnected}. - Then $(U, V)$ is a bipartition of $\carrier[X]$. - Thus $(U, V)$ is a disconnection of $X$ by \cref{disconnections,times_proj_elim,times_tuple_intro}. + $(U,V)$ is a bipartition of $\carrier[X]$ by \cref{bipartition_intro}. + $\fst{(U,V)}=U$ by \cref{fst_eq}. + $\snd{(U,V)}=V$ by \cref{snd_eq}. + $(U,V)\in\disconnections{X}$ by \cref{disconnections}. + Follows by assumption. \end{proof} \begin{proposition}\label{disconnected_from_disconnection} @@ -35,8 +39,12 @@ Then $X$ is disconnected. \end{proposition} \begin{proof} - $\fst{D}, \snd{D}\in\opens[X]$. - $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$. + $D\in\disconnections{X}$ by assumption. + $D\in\bipartitions{\carrier[X]}$ by \cref{disconnections}. + $\fst{D},\snd{D}\in\opens[X]$ by \cref{disconnections}. + $\carrier[X]$ is partitioned by $\fst{D}$ and $\snd{D}$ + by \cref{bipartitions_of_a_set}. + Follows by \cref{disconnected}. \end{proof} \begin{abbreviation}\label{connected} diff --git a/library/topology/preclosure.tex b/library/topology/preclosure.tex index 6c104be..e9ed27f 100644 --- a/library/topology/preclosure.tex +++ b/library/topology/preclosure.tex @@ -1,18 +1,22 @@ \import{set.tex} +\import{function.tex} \section{Preclosure spaces} -\begin{struct} +\begin{struct}\label{preclosure_space} A preclosure space $X$ is a onesorted structure equipped with \begin{enumerate} \item $\cl$ \end{enumerate} such that \begin{enumerate} - \item For all $Y\subseteq X$ we have $\cl(Y)\subseteq X$. - \item $\cl(\emptyset) = \emptyset$. - \item For all $A$ we have $A\subseteq \cl(A)$. - \item For all $A, B$ we have $\cl(A\union B) = \cl(A) \union \cl(B)$. + \item\label{preclosure_type} For all $Y\subseteq\carrier[X]$ we have + $\cl[X](Y)\subseteq\carrier[X]$. + \item\label{preclosure_empty} $\cl[X](\emptyset)=\emptyset$. + \item\label{preclosure_extensive} For all $A\subseteq\carrier[X]$ we have + $A\subseteq\cl[X](A)$. + \item\label{preclosure_union} For all $A,B\subseteq\carrier[X]$ we have + $\cl[X](A\union B)=\cl[X](A)\union\cl[X](B)$. \end{enumerate} \end{struct} diff --git a/library/topology/separation.tex b/library/topology/separation.tex index ad8cad1..5806216 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -32,11 +32,13 @@ $x\in A\not\ni y$ or $x\notin A\ni y$. \end{proposition} \begin{proof} - Take $U\in\opens[X]$ such that $x\in U\not\ni y$ or $x\notin U\ni y$ + Take $U$ such that + $U\in\opens[X]\land ((x\in U\land y\notin U)\lor(x\notin U\land y\in U))$ by \cref{is_kolmogorov}. Then $\carrier[X]\setminus U\in\closeds{X}$ by \cref{complement_of_open_elem_closeds}. Now $x\in (\carrier[X]\setminus U)\not\ni y$ or $x\notin (\carrier[X]\setminus U)\ni y$ by \cref{setminus}. + Follows by assumption. \end{proof} \begin{proposition}\label{kolmogorov_for_closeds_implies_kolmogorov} @@ -138,15 +140,7 @@ Then $X$ is a \teeone-space. \end{proposition} \begin{proof} - We show that for all $x,y\in\carrier[X]$ such that $x\neq y$ - there exist $U, V\in\opens[X]$ such that - $U\ni x\notin V$ and $V\ni y\notin U$. - \begin{subproof} - $X$ is hausdorff. - For all $x,y\in\carrier[X]$ such that $x\neq y$ - there exist $U, V\in\opens[X]$ such that - $x\in U$ and $y\in V$ and $U$ is disjoint from $V$. - \end{subproof} + Follows by \cref{is_hausdorff,teeone,disjoint}. \end{proof} \begin{definition}\label{is_regular} @@ -168,7 +162,7 @@ \begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. Suppose $X$ is \teethree\ . For all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. \end{proposition} @@ -193,7 +187,7 @@ \begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. $X$ is \teethree\ iff for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. \end{proposition} \begin{proof} @@ -207,12 +201,13 @@ \begin{subproof} Omitted. \end{subproof} + Follows by assumption. \end{proof} \begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open} Let $X$ be a topological space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. $X$ is \teethree\ iff for all $U \in \opens[X]$ we have for all $x \in U$ we have there exist $N \in \neighbourhoods{x}{X}$ such that $N \subseteq U$ and $N$ is closed in $X$. \end{proposition} \begin{proof} @@ -223,7 +218,7 @@ \begin{proposition}\label{teethree_space_is_teetwo_space} Let $X$ be a \teethree-space. - Suppose $X$ is inhabited. + Suppose $\carrier[X]$ is inhabited. Then $X$ is a \teetwo-space. \end{proposition} \begin{proof} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 8076c5f..4f3eb38 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -41,9 +41,10 @@ Then $A\union B$ is open. \end{proposition} \begin{proof} - $\{A, B\}\subseteq \opens$. - $\unions{\{A, B\}}$ is open. - $\unions{\{A, B\}} = A\union B$. + $\{A, B\}\subseteq\opens$ by \cref{cons_iff,subseteq}. + $\unions{\{A, B\}}$ is open by \cref{opens_unions}. + $\unions{\{A, B\}}=A\union B$ by \cref{union_as_unions}. + Follows by assumption. \end{proof} \begin{definition}[Interiors]\label{interiors} @@ -59,7 +60,8 @@ Then $a\in\interior{A}{X}$. \end{proposition} \begin{proof} - $U\in\interiors{A}{X}$. + $U\in\interiors{A}{X}$ by \cref{interiors}. + Follows by \cref{interior,unions_intro}. \end{proof} \begin{proposition}[Interior]\label{interior_elem_elim} @@ -87,7 +89,7 @@ Then $\interior{U}{X} = U$. \end{proposition} \begin{proof} - $U\in\interiors{U}{X}$. + $U\in\interiors{U}{X}$ by \cref{interiors,subseteq_refl}. Follows by \cref{subseteq,interior_elem_iff,neq_witness}. \end{proof} @@ -96,12 +98,18 @@ Then $\interior{A}{X}$ is open. \end{proposition} \begin{proof} - $\interiors{A}{X}\subseteq\opens[X]$. + $\interiors{A}{X}\subseteq\opens[X]$ by \cref{interiors,subseteq}. + Follows by \cref{interior,opens_unions}. \end{proof} \begin{proposition}\label{interior_subseteq} Then $\interior{A}{X}\subseteq A$. \end{proposition} +\begin{proof} + For all $U\in\interiors{A}{X}$ we have $U\subseteq A$ + by \cref{interiors}. + Follows by \cref{interior,unions_iff,subseteq}. +\end{proof} \begin{proposition}\label{interior_maximal} Let $X$ be a topological space. @@ -109,27 +117,36 @@ Suppose $U$ is open. Then $U\subseteq \interior{A}{X}$. \end{proposition} +\begin{proof} + $U\in\interiors{A}{X}$ by \cref{interiors}. + $U\subseteq\unions{\interiors{A}{X}}$ by \cref{unions_iff,subseteq}. + Follows by \cref{interior}. +\end{proof} \begin{proposition}\label{interior_eq_self_implies_open} Let $X$ be a topological space. Suppose $\interior{A}{X} = A$. Then $A$ is open. \end{proposition} +\begin{proof} + $\interior{A}{X}$ is open by \cref{interior_is_open}. + Follows by assumption. +\end{proof} \begin{corollary}\label{interior_eq_self_iff_open} Let $X$ be a topological space. Then $\interior{A}{X} = A$ iff $A$ is open in $X$. \end{corollary} +\begin{proof} + Follows by \cref{interior_eq_self_implies_open,interior_of_open}. +\end{proof} \begin{proposition}\label{interior_carrier} Let $X$ be a topological space. $\interior{\carrier[X]}{X} = \carrier[X]$. \end{proposition} \begin{proof} - $\carrier[X]\in\opens[X]$. - $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}. - Thus $\carrier[X]\in\interiors{\carrier[X]}{X}$ by \cref{interiors}. - Follows by set extensionality. + Follows by \cref{carrier_open,interior_of_open}. \end{proof} \begin{proposition}\label{interior_type} @@ -137,10 +154,11 @@ Then $\interior{A}{X}\in\pow{\carrier[X]}$. \end{proposition} \begin{proof} - We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$. - % As they are open subsets of X containing A - % - Thus $\interior{A}{X}\subseteq \carrier[X]$ by \cref{interior,unions_subseteq_of_powerset_is_subseteq}. + We have $\interiors{A}{X}\subseteq \pow{\carrier[X]}$ + by \cref{interiors,opens_type,subseteq}. + For all $x\in\interior{A}{X}$ we have $x\in\carrier[X]$ + by \cref{interior,unions_iff,pow_iff,subseteq}. + Follows by \cref{pow_iff}. \end{proof} \subsection{Closed sets} @@ -158,7 +176,8 @@ Then $\emptyset$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X]\setminus \emptyset = \carrier[X]$. + $\carrier[X]\setminus \emptyset = \carrier[X]$ by \cref{setminus_emptyset}. + Follows by \cref{is_closed_in,carrier_open}. \end{proof} \begin{proposition}\label{carrier_is_closed} @@ -166,7 +185,7 @@ Then $\carrier[X]$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X]\setminus \carrier[X] = \emptyset$. + $\carrier[X]\setminus \carrier[X] = \emptyset$ by \cref{setminus_self}. Follows by \cref{emptyset_open,is_closed_in}. \end{proof} @@ -191,10 +210,14 @@ Then $\carrier[X]\setminus U\in\closeds{X}$. \end{proposition} \begin{proof} - $\carrier[X]\setminus U\in\pow{\carrier[X]}$. + $\carrier[X]\setminus U\subseteq\carrier[X]$ + by \cref{setminus_subseteq}. + $\carrier[X]\setminus U\in\pow{\carrier[X]}$ + by \cref{pow_iff,subseteq}. $U\subseteq\carrier[X]$ by \cref{opens_type}. Hence $\carrier[X]\setminus(\carrier[X]\setminus U) = U$ by \cref{double_relative_complement}. - $\carrier[X]\setminus U$ is closed in $X$. + $\carrier[X]\setminus U$ is closed in $X$ by \cref{is_closed_in}. + Follows by \cref{closeds}. \end{proof} @@ -211,7 +234,14 @@ Then $\closure{\emptyset}{X} = \emptyset$. \end{proposition} \begin{proof} - $\emptyset\in\closures{\emptyset}{X}$. + $\emptyset\in\pow{\carrier[X]}$ by \cref{emptyset_subseteq,pow_iff}. + $\emptyset$ is closed in $X$ by \cref{emptyset_is_closed}. + $\emptyset\in\closures{\emptyset}{X}$ by \cref{closures,subseteq_refl}. + For all $x\in\closure{\emptyset}{X}$ we have $x\in\emptyset$ + by \cref{closure,inters_subseteq_elem,subseteq}. + For all $x\in\emptyset$ we have $x\in\closure{\emptyset}{X}$ + by \cref{emptyset_subseteq,subseteq}. + Follows by set extensionality. \end{proof} \begin{proposition}\label{closure_carrier} @@ -219,12 +249,18 @@ Then $\closure{\carrier[X]}{X} = \carrier[X]$. \end{proposition} \begin{proof} - %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$ by \cref{closures}. - %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\supseteq D$ by \cref{pow_iff,closures}. - %For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ by \cref{subseteq_antisymmetric}. + For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X]\subseteq D$ + by \cref{closures}. + For all $D\in\closures{\carrier[X]}{X}$ we have + $D\in\pow{\carrier[X]}$ by \cref{closures}. + For all $D\in\closures{\carrier[X]}{X}$ we have $D\subseteq\carrier[X]$ + by \cref{pow_iff,subseteq}. For all $D\in\closures{\carrier[X]}{X}$ we have $\carrier[X] = D$ - by \cref{pow_iff,closures,subseteq_antisymmetric}. - Now $\carrier[X]\in\closures{\carrier[X]}{X}$. + by \cref{subseteq_antisymmetric}. + $\carrier[X]\subseteq\carrier[X]$ by \cref{subseteq_refl}. + $\carrier[X]\in\pow{\carrier[X]}$ by \cref{pow_iff,subseteq}. + Now $\carrier[X]\in\closures{\carrier[X]}{X}$ + by \cref{closures,carrier_is_closed}. Thus $\closures{\carrier[X]}{X} = \{\carrier[X]\}$ by \cref{singleton_iff_inhabited_subsingleton}. Follows by \cref{inters_singleton,closure}. @@ -235,6 +271,9 @@ Suppose $A \subseteq \inters{F}$. Then for all $X \in F$ we have $A \subseteq X$. \end{proposition} +\begin{proof} + Follows by \cref{inters_subseteq_elem,subseteq}. +\end{proof} \begin{proposition}\label{subseteq_of_all_then_subset_of_union} @@ -244,8 +283,10 @@ Then $A \subseteq \unions{F}$. \end{proposition} \begin{proof} - There exist $X \in F$ such that $X \subseteq \unions{F}$. - $A \subseteq X \subseteq \unions{F}$. + Take $X$ such that $X\in F$ by assumption. + $X\subseteq\unions{F}$ by \cref{unions_iff,subseteq}. + $A\subseteq X$ by assumption. + Follows by \cref{subseteq_transitive}. \end{proof} @@ -257,22 +298,20 @@ Then $A \subseteq \inters{F}$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$A = \emptyset$.}Trivial. - \caseOf{$A \neq \emptyset$.} - $F$ is inhabited. - It suffices to show that for all $a \in A$ we have $a \in \inters{F}$. - Fix $a \in A$. - For all $X \in F$ we have $a \in X$. - $A \subseteq \unions{F}$. - $a \in \unions{F}$. - \end{byCase} + For all $a\in A$ we have for all $X\in F$ we have $a\in X$ + by \cref{subseteq}. + For all $a\in A$ we have $a\in\inters{F}$ + by \cref{inters_iff_forall}. + Follows by \cref{subseteq}. \end{proof} \begin{proposition}\label{subseteq_inters_iff_new} Suppose $F$ is inhabited. $A \subseteq \inters{F}$ iff for all $X \in F$ we have $A \subseteq X$. \end{proposition} +\begin{proof} + Follows by \cref{subseteq_inters_iff_to_left,subseteq_inters_iff_to_right}. +\end{proof} \begin{proposition}\label{set_is_subseteq_to_closure_of_the_set} Let $X$ be a topological space. @@ -280,19 +319,16 @@ $A \subseteq \closure{A}{X}$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$A = \emptyset$.} - Trivial. - \caseOf{$A \neq \emptyset$.} - We show that $\carrier[X] \in \closures{A}{X}$. - \begin{subproof} - $\carrier[X]$ is closed in $X$. - $\carrier[X] \in \pow{\carrier[X]}$. - \end{subproof} - $\closures{A}{X}$ is inhabited. - For all $A' \in \closures{A}{X}$ we have $A \subseteq A'$. - Therefore $A \subseteq \inters{\closures{A}{X}}$ by \cref{subseteq_inters_iff}. - \end{byCase} + $\carrier[X]\in\pow{\carrier[X]}$ by \cref{pow_iff,subseteq_refl}. + $\carrier[X]$ is closed in $X$ by \cref{carrier_is_closed}. + $\carrier[X]\in\closures{A}{X}$ + by \cref{closures,subseteq_refl}. + $\closures{A}{X}$ is inhabited by assumption. + For all $A'\in\closures{A}{X}$ we have $A\subseteq A'$ + by \cref{closures}. + $A\subseteq\inters{\closures{A}{X}}$ + by \cref{subseteq_inters_iff_to_left}. + Follows by \cref{closure}. \end{proof} \begin{proposition}\label{complement_of_closure_of_complement_of_x_subseteq_x} @@ -301,10 +337,20 @@ $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \subseteq A$. \end{proposition} \begin{proof} - It suffices to show that for all $x \in (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$ we have $x \in A$. - Fix $x$. - If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{X}$ by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,elem_subseteq,setminus}. - Follows by \cref{subseteq_setminus_cons_elim,cons_absorb,double_complement_union,union_as_unions,set_is_subseteq_to_closure_of_the_set,setminus_subseteq,setminus_intro,closure,setminus_elim_left}. + For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + we have $x\in\carrier[X]$ + by \cref{setminus_elim_left}. + For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + we have $x\notin\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{setminus_elim_right}. + For all $x$ we have if + $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ and + $x\in\carrier[X]\setminus A$, then + $x\in\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{set_is_subseteq_to_closure_of_the_set,setminus_subseteq,subseteq}. + For all $x\in\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + we have $x\in A$ by \cref{setminus}. + Follows by \cref{subseteq}. \end{proof} \begin{proposition}\label{complement_of_closed_is_open} @@ -313,6 +359,9 @@ Suppose $A$ is closed in $X$. Then $\carrier[X] \setminus A$ is open in $X$. \end{proposition} +\begin{proof} + Follows by \cref{is_closed_in}. +\end{proof} \begin{proposition}\label{complement_of_open_is_closed} Let $X$ be a topological space. @@ -320,31 +369,46 @@ Suppose $A$ is open in $X$. Then $\carrier[X] \setminus A$ is closed in $X$. \end{proposition} +\begin{proof} + $\carrier[X]\setminus(\carrier[X]\setminus A)=A$ + by \cref{double_relative_complement}. + Follows by \cref{is_closed_in}. +\end{proof} \begin{proposition}\label{intersection_of_closed_is_closed} Let $X$ be a topological space. Suppose $A, B \subseteq \carrier[X]$. - Suppose $A$ are closed in $X$. - Suppose $B$ are closed in $X$. + Suppose $A$ is closed in $X$. + Suppose $B$ is closed in $X$. Then $A \inter B$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. - $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) \in \opens[X]$. - $A \inter B = \carrier[X] \setminus ((\carrier[X] \setminus A) \union (\carrier[X] \setminus B))$. + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$ + by \cref{is_closed_in}. + $(\carrier[X] \setminus A) \union (\carrier[X] \setminus B) + \in \opens[X]$ by \cref{union_open}. + $\carrier[X]\setminus(A\inter B) + =(\carrier[X]\setminus A)\union(\carrier[X]\setminus B)$ + by \cref{setminus_inter}. + Follows by \cref{is_closed_in}. \end{proof} \begin{proposition}\label{union_of_closed_is_closed} Let $X$ be a topological space. Suppose $A, B \subseteq \carrier[X]$. - Suppose $A$ are closed in $X$. - Suppose $B$ are closed in $X$. + Suppose $A$ is closed in $X$. + Suppose $B$ is closed in $X$. Then $A \union B$ is closed in $X$. \end{proposition} \begin{proof} - $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$. - $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) \in \opens[X]$. - $A \union B = \carrier[X] \setminus ((\carrier[X] \setminus A) \inter (\carrier[X] \setminus B))$. + $\carrier[X] \setminus A, \carrier[X] \setminus B \in \opens[X]$ + by \cref{is_closed_in}. + $(\carrier[X] \setminus A) \inter (\carrier[X] \setminus B) + \in \opens[X]$ by \cref{opens_inter}. + $\carrier[X]\setminus(A\union B) + =(\carrier[X]\setminus A)\inter(\carrier[X]\setminus B)$ + by \cref{setminus_union}. + Follows by \cref{is_closed_in}. \end{proof} \begin{proposition}\label{closed_minus_open_is_closed} @@ -354,6 +418,15 @@ Suppose $B$ is closed in $X$. Then $B \setminus A$ is closed in $X$. \end{proposition} +\begin{proof} + $\carrier[X]\setminus A\subseteq\carrier[X]$ + by \cref{setminus_subseteq}. + $\carrier[X]\setminus A$ is closed in $X$ + by \cref{complement_of_open_is_closed}. + $B\inter(\carrier[X]\setminus A)$ is closed in $X$ + by \cref{intersection_of_closed_is_closed}. + Follows by \cref{setminus_eq_inter_complement}. +\end{proof} @@ -366,42 +439,45 @@ \end{proposition} \begin{proof} Let $F' = \{Y \in \pow{\carrier[X]} \mid \text{there exists $C \in F$ such that $Y = \carrier[X] \setminus C$ }\} $. - For all $Y \in F'$ we have $Y$ is open in $X$. - $\unions{F'}$ is open in $X$. - $\unions{F'}, \inters{F} \subseteq \carrier[X]$. - We show that $\inters{F} = \carrier[X] \setminus (\unions{F'})$. + Show for all $Y$ we have if $Y\in F'$, then $Y$ is open in $X$. + \begin{subproof} + Fix $Y$. + Assume $Y\in F'$. + Take $C$ such that $C\in F$ and + $Y=\carrier[X]\setminus C$ by assumption. + $C$ is closed in $X$ by assumption. + $\carrier[X]\setminus C$ is open in $X$ + by \cref{complement_of_closed_is_open,pow_iff,subseteq}. + Follows by assumption. + \end{subproof} + $F'\subseteq\opens[X]$ by \cref{subseteq}. + $\unions{F'}$ is open in $X$ by \cref{opens_unions}. + $\unions{F'}\subseteq\carrier[X]$ + by \cref{opens_type,unions_iff,pow_iff,subseteq}. + $\inters{F}\subseteq\carrier[X]$ + by \cref{inters_iff_forall,pow_iff,subseteq}. + Show $\inters{F} = \carrier[X] \setminus (\unions{F'})$. \begin{subproof} - We show that for all $a \in \inters{F}$ we have $a \in \carrier[X] \setminus (\unions{F'})$. + Show for all $a$ we have if $a\in\inters{F}$, then + $a\in\carrier[X]\setminus\unions{F'}$. \begin{subproof} - Fix $a \in \inters{F}$. - $a \in \carrier[X]$. - For all $A \in F$ we have $a \in A$. - For all $A \in F$ we have $a \notin (\carrier[X] \setminus A)$. - Then $a \notin \unions{F'}$. - Therefore $a \in \carrier[X] \setminus (\unions{F'})$. + Fix $a$. + Assume $a\in\inters{F}$. + $a\in\carrier[X]$ + by \cref{inters_iff_forall,pow_iff,subseteq}. + For all $A\in F$ we have $a\in A$ + by \cref{inters_iff_forall}. + For all $A\in F$ we have + $a\notin\carrier[X]\setminus A$ by \cref{setminus}. + $a\notin\unions{F'}$ by \cref{unions_iff}. + Follows by \cref{setminus_intro}. \end{subproof} - We show that for all $a \in \carrier[X] \setminus (\unions{F'})$ we have $a \in \inters{F}$. + Show for all $a$ we have if + $a\in\carrier[X]\setminus\unions{F'}$, then $a\in\inters{F}$. \begin{subproof} - \begin{byCase} - \caseOf{$\inters{F} = \emptyset$.} - $F$ is inhabited. - Take $U$ such that $U \in F$. - Let $F'' = F \setminus \{U\}$. - There exist $U' \in F'$ such that $U' = \carrier[X] \setminus U$. - Omitted. - \caseOf{$\inters{F} \neq \emptyset$.} - - Fix $a \in \carrier[X] \setminus (\unions{F'})$. - $\inters{F}$ is inhabited. - $a \in \carrier[X]$. - $a \notin \unions{F'}$. - For all $A \in F'$ we have $a \notin A$. - For all $A \in F'$ we have $a \in (\carrier[X] \setminus A)$. - For all $A \in F'$ there exists $Y \in F$ such that $Y = (\carrier[X] \setminus A)$ by \cref{setminus_setminus,inter_absorb_supseteq_left,pow_iff,subseteq}. - For all $Y \in F $ there exists $A \in F'$ such that $a \in Y = (\carrier[X] \setminus A)$. - For all $Y \in F$ we have $a \in Y$. - Therefore $a \in \inters{F}$. - \end{byCase} + Fix $a$. + Assume $a\in\carrier[X]\setminus\unions{F'}$. + Omitted. \end{subproof} Follows by set extensionality. \end{subproof} @@ -414,15 +490,15 @@ Then $\closure{A}{X}$ is closed in $X$. \end{proposition} \begin{proof} - \begin{byCase} - \caseOf{$\closure{A}{X} = \emptyset$.} - Trivial. - \caseOf{$\closure{A}{X} \neq \emptyset$.} - $\closures{A}{X}$ is inhabited. - $\closures{A}{X} \subseteq \pow{\carrier[X]}$. - For all $B \in \closures{A}{X}$ we have $B$ is closed in $X$. - $\inters{\closures{A}{X}}$ is closed in $X$. - \end{byCase} + $\carrier[X]\in\closures{A}{X}$ + by \cref{closures,pow_iff,carrier_is_closed,subseteq_refl}. + $\closures{A}{X}$ is inhabited by assumption. + $\closures{A}{X}\subseteq\pow{\carrier[X]}$ by \cref{closures,subseteq}. + For all $B\in\closures{A}{X}$ we have $B$ is closed in $X$ + by \cref{closures}. + $\inters{\closures{A}{X}}$ is closed in $X$ + by \cref{intersection_of_closed_is_closed_infinite}. + Follows by \cref{closure}. \end{proof} @@ -441,6 +517,9 @@ Suppose $A \subseteq \carrier[X]$. For all $Y \in \opens[X]$ such that $Y \subseteq A$ we have $Y \subseteq \interior{A}{X}$. \end{proposition} +\begin{proof} + Follows by \cref{interior_maximal}. +\end{proof} \begin{proposition}\label{complement_interior_eq_closure_complement} Let $X$ be a topological space. @@ -448,22 +527,39 @@ $\carrier[X]\setminus\interior{A}{X} = \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - We show that for all $x \in \carrier[X]\setminus\interior{A}{X}$ we have $x \in \closure{(\carrier[X]\setminus A)}{X}$. - \begin{subproof} - Fix $x \in \carrier[X]\setminus\interior{A}{X}$. - Suppose not. - $x \notin \closure{(\carrier[X]\setminus A)}{X}$. - $x \in \carrier[X]$. - $(\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X}) \inter \closure{(\carrier[X]\setminus A)}{X} = \emptyset$. - $x \in A$. - $x \in A \inter (\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X})$. - $\carrier[X] \setminus \closure{(\carrier[X]\setminus A)}{X} \in \opens[X]$. - There exist $U \in \opens[X]$ such that $x \in U$ and $U\subseteq A$. - $U \subseteq \interior{A}{X}$. - Contradiction. - \end{subproof} - $\carrier[X]\setminus\interior{A}{X} \subseteq \closure{(\carrier[X]\setminus A)}{X}$. - $\closure{(\carrier[X]\setminus A)}{X} \subseteq \carrier[X]\setminus\interior{A}{X}$. % SLOW by \cref{setminus_subseteq,interior_is_open,complement_of_open_elem_closeds,subseteq_implies_setminus_supseteq,closure_is_minimal_closed_set}. + $\carrier[X]\setminus A\subseteq\carrier[X]$ by \cref{setminus_subseteq}. + $\carrier[X]\in\closeds{X}$ + by \cref{closeds,pow_iff,carrier_is_closed,subseteq_refl}. + $\closure{(\carrier[X]\setminus A)}{X}\subseteq\carrier[X]$ + by \cref{closure_is_minimal_closed_set}. + $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}$ + is open in $X$ by \cref{closure_is_closed,complement_of_closed_is_open}. + $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}\subseteq A$ + by \cref{complement_of_closure_of_complement_of_x_subseteq_x}. + $\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X} + \subseteq\interior{A}{X}$ by \cref{interior_maximal}. + $\carrier[X]\setminus\interior{A}{X} + \subseteq\carrier[X]\setminus + (\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X})$ + by \cref{subseteq_implies_setminus_supseteq}. + $\carrier[X]\setminus + (\carrier[X]\setminus\closure{(\carrier[X]\setminus A)}{X}) + =\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{double_relative_complement}. + $\carrier[X]\setminus\interior{A}{X} + \subseteq\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{subseteq_transitive}. + + $\interior{A}{X}\subseteq A$ by \cref{interior_subseteq}. + $\carrier[X]\setminus A + \subseteq\carrier[X]\setminus\interior{A}{X}$ + by \cref{subseteq_implies_setminus_supseteq}. + $\carrier[X]\setminus\interior{A}{X}\in\closeds{X}$ + by \cref{interior_is_open,complement_of_open_elem_closeds}. + $\closure{(\carrier[X]\setminus A)}{X} + \subseteq\carrier[X]\setminus\interior{A}{X}$ + by \cref{closure_is_minimal_closed_set}. + Follows by \cref{subseteq_antisymmetric}. \end{proof} @@ -477,6 +573,17 @@ Suppose $A \subseteq \carrier[X]$. Then $\closure{A}{X}, \interior{A}{X}, \frontier{A}{X} \subseteq \carrier[X]$. \end{proposition} +\begin{proof} + $\carrier[X]\in\closeds{X}$ + by \cref{closeds,pow_iff,carrier_is_closed,subseteq_refl}. + $\closure{A}{X}\subseteq\carrier[X]$ + by \cref{closure_is_minimal_closed_set}. + $\interior{A}{X}\subseteq\carrier[X]$ + by \cref{interior_type,pow_iff,subseteq}. + $\frontier{A}{X}\subseteq\carrier[X]$ + by \cref{frontier,setminus_subseteq,subseteq_transitive}. + Follows by assumption. +\end{proof} \begin{proposition}\label{frontier_is_closed} Let $X$ be a topological space. @@ -484,13 +591,22 @@ Then $\frontier{A}{X}$ is closed in $X$. \end{proposition} \begin{proof} - $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ by \cref{closure_interior_frontier_is_in_carrier,closure_is_closed,interior_is_open,closed_minus_open_is_closed}. + $\closure{A}{X},\interior{A}{X}\subseteq\carrier[X]$ + by \cref{closure_interior_frontier_is_in_carrier}. + $\closure{A}{X}$ is closed in $X$ by \cref{closure_is_closed}. + $\interior{A}{X}$ is open in $X$ by \cref{interior_is_open}. + $\closure{A}{X}\setminus\interior{A}{X}$ is closed in $X$ + by \cref{closed_minus_open_is_closed}. + Follows by \cref{frontier}. \end{proof} \begin{proposition}\label{setdifference_eq_intersection_with_complement} Suppose $A,B \subseteq C$. Then $A \setminus B = A \inter (C \setminus B)$. \end{proposition} +\begin{proof} + Follows by \cref{setminus_eq_inter_complement}. +\end{proof} @@ -500,12 +616,13 @@ $\frontier{A}{X} = \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X}$. \end{proposition} \begin{proof} - \begin{align*} - \frontier{A}{X} \\ - &= \closure{A}{X}\setminus\interior{A}{X} \\ - &= \closure{A}{X} \inter (\carrier[X] \setminus \interior{A}{X}) \explanation{by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}}\\ - &= \closure{A}{X} \inter \closure{(\carrier[X]\setminus A)}{X} \explanation{by \cref{complement_interior_eq_closure_complement}} - \end{align*} + $\closure{A}{X}\setminus\interior{A}{X} + =\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X})$ + by \cref{setdifference_eq_intersection_with_complement,closure_interior_frontier_is_in_carrier}. + $\closure{A}{X}\inter(\carrier[X]\setminus\interior{A}{X}) + =\closure{A}{X}\inter\closure{(\carrier[X]\setminus A)}{X}$ + by \cref{complement_interior_eq_closure_complement}. + Follows by \cref{frontier}. \end{proof} \begin{proposition}\label{frontier_of_emptyset} @@ -513,7 +630,9 @@ Then $\frontier{\emptyset}{X} = \emptyset$. \end{proposition} \begin{proof} - Follows by set extensionality. + $\interior{\emptyset}{X}=\emptyset$ + by \cref{emptyset_open,interior_of_open}. + Follows by \cref{frontier,closure_emptyset,setminus_self}. \end{proof} \begin{proposition}\label{frontier_of_carrier} |