diff options
Diffstat (limited to 'library/topology')
| -rw-r--r-- | library/topology/continuous.tex | 29 | ||||
| -rw-r--r-- | library/topology/separation.tex | 98 | ||||
| -rw-r--r-- | library/topology/topological-space.tex | 17 |
3 files changed, 103 insertions, 41 deletions
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex new file mode 100644 index 0000000..6a32353 --- /dev/null +++ b/library/topology/continuous.tex @@ -0,0 +1,29 @@ +\import{topology/topological-space.tex} +\import{relation.tex} + +\begin{definition}\label{continuous} + $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$. +\end{definition} + +\begin{proposition}\label{continuous_definition_by_closeds} + Let $X$ be a topological space. + Let $Y$ be a topological space. + Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. +\end{proposition} +\begin{proof} + Omitted. + %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$. + %\begin{subproof} + % Suppose $f$ is continuous. + % Fix $U \in \closeds{Y}$. + % $\carrier[Y] \setminus U$ is open in $Y$. + % Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$. + % Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$. + % $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$. + % $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$. + %\end{subproof} + %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous. + %\begin{subproof} + % Omitted. + %\end{subproof} +\end{proof} diff --git a/library/topology/separation.tex b/library/topology/separation.tex index c53b6a8..0c68290 100644 --- a/library/topology/separation.tex +++ b/library/topology/separation.tex @@ -77,25 +77,26 @@ Then $\{x\}$ is closed in $X$. \end{proposition} \begin{proof} - Let $V = \{ U \in \opens[X] \mid x \notin U\}$. - For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$. - For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$. - - $\unions{V} \in \opens[X]$. - For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$. - We show that $\carrier[X] \setminus \{x\} = \unions{V}$. - \begin{subproof} - We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$. - \begin{subproof} - Fix $y \in \carrier[X] \setminus \{x\}$. - $y \neq x$. - $y \in \carrier[X]$. - $y \in \unions{V}$. - \end{subproof} - For all $y \in \unions{V}$ we have $y \notin \{x\}$. - For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. - Follows by set extensionality. - \end{subproof} + Omitted. + %Let $V = \{ U \in \opens[X] \mid x \notin U\}$. + %For all $y \in \carrier[X]$ such that $x \neq y$ there exist $U \in \opens[X]$ such that $x \notin U \ni y$ by \cref{carrier_open,teeone}. + %For all $y \in \carrier[X]$ such that $y \neq x$ there exists $U \in V$ such that $y \in U$. + % + %$\unions{V} \in \opens[X]$. + %For all $y \in \carrier[X]$ such that $x \neq y$ we have $y \in \unions{V}$. + %We show that $\carrier[X] \setminus \{x\} = \unions{V}$. + %\begin{subproof} + % We show that for all $y \in \carrier[X] \setminus \{x\}$ we have $y \in \unions{V}$. + % \begin{subproof} + % Fix $y \in \carrier[X] \setminus \{x\}$. + % $y \neq x$. + % $y \in \carrier[X]$. + % $y \in \unions{V}$. + % \end{subproof} + % For all $y \in \unions{V}$ we have $y \notin \{x\}$. + % For all $y \in \unions{V}$ we have $y \in \carrier[X] \setminus \{x\}$. + % Follows by set extensionality. + %\end{subproof} \end{proof} % % Conversely, if \{x\} is open, then for any y distinct from x we can use @@ -163,38 +164,59 @@ $X$ is a \teethree-space iff $X$ is a topological space and $X$ is \teethree\ . \end{abbreviation} -\begin{proposition}\label{eqvilance_teethree_closed_neighbourhood_in_open} +\begin{proposition}\label{teethree_implies_closed_neighbourhood_in_open} Let $X$ be a topological space. Suppose $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$. + 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} \begin{proof} + Omitted. + %%Suppose $X$ is regular and kolmogorov. + %Fix $U \in \opens[X]$. + %Fix $x \in U$. + %Let $C = \carrier[X] \setminus U$. + %Then $C \in \closeds{X}$. + %$x \notin C$. + %$x \in \carrier[X]$. + %We show that there exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$. + %We show that $B \subseteq (\carrier[X] \setminus A)$. + %$(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$. + %$(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$. + %$x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$. + %Let $N = (\carrier[X] \setminus A)$. + %Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$. + %$N \in \neighbourhoods{x}{X}$. +\end{proof} - We show that if $X$ is \teethree\ then 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$. +\begin{proposition}\label{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods} + Let $X$ be a topological space. + Suppose $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} + We show that if $X$ is \teethree\ then for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$. \begin{subproof} - Suppose $X$ is regular and kolmogorov. - Fix $U \in \opens[X]$. - Fix $x \in U$. - Let $C = \carrier[X] \setminus U$. - Then $C \in \closeds{X}$. - $x \notin C$. - $x \in \carrier[X]$. - There exists $A,B \in \opens[X]$ such that $x \in B$ and $C \subseteq A$ and $A \inter B = \emptyset$ by \cref{is_regular}. - $B \subseteq (\carrier[X] \setminus A)$. - $(\carrier[X] \setminus A) \subseteq (\carrier[X] \setminus (\carrier[X] \setminus U))$. - $(\carrier[X] \setminus (\carrier[X] \setminus U)) = U$. - $x \in B \subseteq (\carrier[X] \setminus A) \subseteq U$. - Let $N = (\carrier[X] \setminus A)$. - Then $N \in \closeds{X}$ and $x \in N$ and $N \subseteq U$. - Particularly, $N \in \neighbourhoods{x}{X}$. + %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$. + Omitted. \end{subproof} - We show that if 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$ then $X$ is \teethree\ . + + We show that if for all $H \in \closeds{X}$ such that $F = \{ N \in \neighbourhoodsSet{H}{X} \mid N \in \closeds{X}\}$ we have $H = \inters{F}$ then $X$ is \teethree\ . \begin{subproof} Omitted. \end{subproof} \end{proof} +\begin{proposition}\label{teethree_iff_closed_neighbourhood_in_open} + Let $X$ be a topological space. + Suppose $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} + Omitted. + %Follows by \cref{teethree_iff_each_closed_is_intersection_of_its_closed_neighborhoods,teethree_implies_closed_neighbourhood_in_open}. +\end{proof} \begin{proposition}\label{teethree_space_is_teetwo_space} diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex index 8da29d3..f8bcb93 100644 --- a/library/topology/topological-space.tex +++ b/library/topology/topological-space.tex @@ -1,5 +1,6 @@ \import{set.tex} \import{set/powerset.tex} +\import{set/cons.tex} \section{Topological spaces} @@ -67,7 +68,8 @@ such that $a\in U\subseteq A$. \end{proposition} \begin{proof} - Take $U\in\interiors{A}{X}$ such that $a\in U$. + Omitted. + %Take $U\in\interiors{A}{X}$ such that $a\in U$. \end{proof} \begin{proposition}[Interior]\label{interior_elem_iff} @@ -175,6 +177,9 @@ Suppose $B$ is closed in $X$. Then $A \setminus B$ is open in $X$. \end{proposition} +\begin{proof} + Follows by \cref{setminus_eq_emptyset_iff_subseteq,is_closed_in,opens_inter,inter_comm_left,setminus_union,inter_assoc,inter_setminus,inter_lower_left,inter_lower_right,setminus_subseteq,double_complement,setminus_setminus,setminus_eq_inter_complement,setminus_self,setminus_inter,union_comm,emptyset_subseteq,setminus_partition}. +\end{proof} \begin{definition}[Closed sets]\label{closeds} $\closeds{X} = \{ A\in\pow{\carrier[X]}\mid\text{$A$ is closed in $X$}\}$. @@ -297,7 +302,8 @@ \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$. - If $x \in \carrier[X]\setminus A$ then $x \in \closure{(\carrier[X]\setminus A)}{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}. \end{proof} \begin{proposition}\label{complement_of_closed_is_open} @@ -381,6 +387,7 @@ 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'})$. @@ -389,7 +396,7 @@ $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)$. + 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}$. @@ -522,3 +529,7 @@ \begin{definition}\label{neighbourhoods} $\neighbourhoods{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\in U\subseteq N\}$. \end{definition} + +\begin{definition}\label{neighbourhoods_set} + $\neighbourhoodsSet{x}{X} = \{N\in\pow{\carrier[X]} \mid \exists U\in\opens[X]. x\subseteq U\subseteq N\}$. +\end{definition} |