diff options
Diffstat (limited to 'library/topology/topological-space.tex')
| -rw-r--r-- | library/topology/topological-space.tex | 375 |
1 files changed, 247 insertions, 128 deletions
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} |