diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/numbers.tex | 10 | ||||
| -rw-r--r-- | library/topology/real-topological-space.tex | 200 |
2 files changed, 194 insertions, 16 deletions
diff --git a/library/numbers.tex b/library/numbers.tex index 8624260..406553e 100644 --- a/library/numbers.tex +++ b/library/numbers.tex @@ -792,7 +792,15 @@ Laws of the order on the reals \end{definition} \begin{definition}\label{intervalopen_infinite_right} - $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid a < x\}$. + $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid x > a\}$. +\end{definition} + +\begin{definition}\label{intervalclosed_infinite_left} + $\intervalclosedInfiniteLeft{b} = \{ x \in \reals \mid x \leq b\}$. +\end{definition} + +\begin{definition}\label{intervalclosed_infinite_right} + $\intervalclosedInfiniteRight{a} = \{ x \in \reals \mid x \geq a\}$. \end{definition} diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex index b3efa20..e5e17ef 100644 --- a/library/topology/real-topological-space.tex +++ b/library/topology/real-topological-space.tex @@ -580,28 +580,198 @@ For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$. \end{proposition} \begin{proof} - Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$. - Let $f(x) = \neg{x}$ for $x \in \reals$. - $f$ is a function from $\reals$ to $\reals$. - We show that $f$ is continuous. + Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteRight{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta} \}$. + We show that for all $x \in \intervalopenInfiniteRight{a}$ we have there exists $e \in E$ such that $x \in e$. \begin{subproof} - It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$. - Fix $b \in \topoBasisReals$. - Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$. - Let $y = \neg{x}$. - It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}. - It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$. - Follows by set extensionality. + Fix $x \in \intervalopenInfiniteRight{a}$. + Then $a < x$. + Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$. + $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_right}. + $a \notin \epsBall{x}{\delta'}$. + $\epsBall{x}{\delta'} \in E$. \end{subproof} - $\intervalopenInfiniteLeft{a} \in \opens[\reals]$. - We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$. + $E \subseteq \topoBasisReals$. + We show that $\unions{E} = \intervalopenInfiniteRight{a}$. \begin{subproof} - Omitted. + We show that $\unions{E} \subseteq \intervalopenInfiniteRight{a}$. + \begin{subproof} + It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteRight{a}$. + Fix $x \in \unions{E}$. + Take $e \in E$ such that $x \in e$. + $x \in \reals$. + Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}. + $\epsBall{x'}{\delta'} \in E$. + We show that for all $y \in e$ we have $y > a$. + \begin{subproof} + Fix $y \in e$. + Then $y \in \epsBall{x'}{\delta'}$. + $e = \epsBall{x'}{\delta'}$. + There exists $x'' \in \intervalopenInfiniteRight{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$. + Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteRight{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$. + Suppose not. + Take $y' \in e$ such that $y' < a$. + $x'' > a$. + $(x'' - \delta'') < y' < (x'' + \delta'')$. + $(x'' - \delta'') < x'' < (x'' + \delta'')$. + Then $x'' > a > y'$. + Therefore $(x'' - \delta'') > a > (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_right,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq,epsball_are_connected_in_reals,subseteq}. + Then $a \in e$ by \cref{reals_order_is_transitive,reals_order_total,reals_add,realsplus,epsball_are_connected_in_reals,intervalopen_infinite_right,neq_witness}. + Contradiction. + \end{subproof} + $x > a$. + Then $x \in \intervalopenInfiniteRight{a}$. + \end{subproof} + We show that $\intervalopenInfiniteRight{a} \subseteq \unions{E}$. + \begin{subproof} + Trivial. + \end{subproof} \end{subproof} - Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}. + $\unions{E} \in \opens[\reals]$. + + %Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$. + %Let $f(x) = \neg{x}$ for $x \in \reals$. + %$f$ is a function from $\reals$ to $\reals$. + %We show that $f$ is continuous. + %\begin{subproof} + % It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$. + % Fix $b \in \topoBasisReals$. + % Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$. + % Let $y = \neg{x}$. + % It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}. + % It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$. + % $\preimg{f}{\epsBall{x}{\epsilon}} \subseteq \reals$. + % $\epsBall{y}{\epsilon} \subseteq \reals$ by \cref{intervalopen,subseteq,minus,epsilon_ball}. + % %It suffices to show that for all $x \in \reals$ we have $x \in \epsBall{y}{\epsilon}$ iff $x \in \preimg{f}{\epsBall{x}{\epsilon}}$. + % %Fix $x \in \reals$. + % Let $u = (y - \epsilon)$. + % Let $v = (y + \epsilon)$. + % $u = \neg{(x - \epsilon)}$. + % $v = \neg{(x + \epsilon)}$. + % %$v - u = \epsilon + \epsilon$. + % We show that for all $z \in \epsBall{y}{\epsilon}$ we have $z \in \preimg{f}{\epsBall{x}{\epsilon}}$. + % \begin{subproof} + % Fix $z \in \epsBall{y}{\epsilon}$. + % Then $u < z < v$. + % Let $z' = z - u$. + % Then $z = u + z'$. + % Suppose not. + % Let $h = \neg{z}$. + % $\neg{h} = \neg{\neg{z}}$. + % $\neg{h} = z$. + % Then $f(h) = \neg{h}$. + % $f(h) = z$. + % Then $z \in \preimg{f}{\{h\}}$. +% + % \end{subproof} + % We show that for all $z \in \preimg{f}{\epsBall{x}{\epsilon}}$ we have $z \in \epsBall{y}{\epsilon}$. + % \begin{subproof} + % Fix $z \in \preimg{f}{\epsBall{x}{\epsilon}}$. + % Take $h \in \epsBall{x}{\epsilon}$ such that $f(h) = z$. + % \end{subproof} + % Follows by set extensionality. + %\end{subproof} + %$\intervalopenInfiniteLeft{a} \in \opens[\reals]$. + %We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$. + %\begin{subproof} + % Omitted. + %\end{subproof} + %Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}. +\end{proof} + +\begin{lemma}\label{reals_as_union_of_open_closed_intervals1} + Suppose $a,b \in \reals$. + Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$. +\end{lemma} +\begin{proof} + We show that for all $x \in \reals$ we have $x \in (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b})$. + \begin{subproof} + Fix $x \in \reals$. + \end{subproof} +\end{proof} + +\begin{lemma}\label{reals_as_union_of_open_closed_intervals2} + Suppose $a \in \reals$. + Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalclosedInfiniteRight{a}$. +\end{lemma} +\begin{proof} + It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$. + Trivial. +\end{proof} + +\begin{lemma}\label{reals_as_union_of_open_closed_intervals3} + Suppose $a \in \reals$. + Then $\reals = \intervalopenInfiniteRight{a} \union \intervalclosedInfiniteLeft{a}$. +\end{lemma} +\begin{proof} + It suffices to show that for all $x \in \reals$ we have either $x \in \intervalclosedInfiniteLeft{a}$ or $x \in \intervalopenInfiniteRight{a}$. + Trivial. +\end{proof} + +\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_right} + Suppose $a \in \reals$. + Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$. +\end{lemma} + +\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left} + Suppose $a \in \reals$. + Then $\intervalopenInfiniteLeft{a} \inter \intervalclosedInfiniteRight{a} = \emptyset$. +\end{lemma} + +\begin{proposition}\label{closedinterval_infinite_right_in_closeds} + Suppose $a \in \reals$. + Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$. +\end{proposition} +\begin{proof} + $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$. +\end{proof} + +\begin{proposition}\label{closedinterval_infinite_left_in_closeds} + Suppose $a \in \reals$. + Then $\intervalclosedInfiniteLeft{a} \in \closeds{\reals}$. +\end{proposition} +\begin{proof} + $\intervalclosedInfiniteLeft{a} = \reals \setminus \intervalopenInfiniteRight{a}$. +\end{proof} + +\begin{proposition}\label{closedinterval_eq_openintervals_setminus_reals} + Suppose $a,b \in \reals$. + Then $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$. +\end{proposition} +\begin{proof} + We have $\intervalclosed{a}{b} \subseteq \reals$. + We show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$. + \begin{subproof} + We show that for all $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$ we have $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$. + \begin{subproof} + Fix $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$. + Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$. + Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$. + \end{subproof} + We show that for all $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$ we have $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$. + \begin{subproof} + Fix $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$. + Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$. + Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$. + \end{subproof} + \end{subproof} + We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$. + \begin{subproof} + For all $x \in \intervalclosedInfiniteRight{a}$ we have $x \geq a$. + For all $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ we have $x \geq a$. + Follows by set extensionality. + \end{subproof} + $\reals \setminus \intervalopenInfiniteRight{b} = \intervalclosedInfiniteLeft{b}$. + It suffices to show that $\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a} = \intervalclosed{a}{b}$. + For all $x \in \intervalclosed{a}{b}$ we have $a \leq x \leq b$. + For all $x \in (\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a})$ we have $a \leq x \leq b$. + Follows by set extensionality. \end{proof} \begin{proposition}\label{closedinterval_is_closed} Suppose $a,b \in \reals$. Then $\intervalclosed{a}{b} \in \closeds{\reals}$. \end{proposition} +\begin{proof} + We have $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$. + It suffices to show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$ by \cref{closeds,setminus_subseteq,powerset_intro,closed_minus_open_is_closed,opens_type,subseteq_refl,union_open,is_closed_in,reals_carrier_reals,setminus_self,emptyset_open,reals_is_topological_space,openinterval_infinite_left_in_opens,openinterval_infinite_right_in_opens}. +\end{proof} |