\import{set.tex}
\import{set/cons.tex}
\import{set/powerset.tex}
\import{set/fixpoint.tex}
\import{set/product.tex}
\import{topology/topological-space.tex}
\import{topology/separation.tex}
\import{topology/continuous.tex}
\import{topology/basis.tex}
\import{numbers.tex}
\import{function.tex}


\section{The canonical topology on $\mathbb{R}$}

\begin{definition}\label{topological_basis_reals_eps_ball}
    $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
\end{definition}

\begin{axiom}\label{reals_carrier_reals}
    $\carrier[\reals] = \reals$.
\end{axiom}

\begin{lemma}\label{intervals_are_connected_in_reals}
    Suppose $a,b \in \reals$.
    Then for all $c \in \reals$ such that $a < c < b$ we have $c \in \intervalopen{a}{b}$.
\end{lemma}

\begin{lemma}\label{epsball_are_subset_reals_elem}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$.
    Then for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \reals$.
\end{lemma}

\begin{lemma}\label{intervalopen_iff}
    Suppose $a,b,c \in \reals$.
    Suppose $a < b$.
    $c \in \intervalopen{a}{b}$ iff $a < c < b$.
\end{lemma}

\begin{lemma}\label{epsball_are_subseteq_reals_set}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$.
    Then $\epsBall{x}{\epsilon} \subseteq \reals$.
\end{lemma}

\begin{lemma}\label{epsball_are_subset_reals_set}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$.
    Then $\epsBall{x}{\epsilon} \subset \reals$.
\end{lemma}

\begin{lemma}\label{reals_order_minus_positiv}
    Suppose $x,y \in \reals$.
    Suppose $\zero < y$.
    $x - y < x$.
\end{lemma}

\begin{lemma}\label{realsplus_bigger_zero}
    For all $x \in \realsplus$ we have $\zero < x$.
\end{lemma}

\begin{lemma}\label{realsplus_in_reals}
    For all $x \in \realsplus$ we have $x \in \reals$.
\end{lemma}

\begin{lemma}\label{epsball_are_inhabited}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$.
    Then $\epsBall{x}{\epsilon}$ is inhabited.
\end{lemma}
\begin{proof}
    $x < x + \epsilon$.
    $x - \epsilon < x$.
    $x \in \epsBall{x}{\epsilon}$.
\end{proof}

\begin{lemma}\label{reals_elem_inbetween}
    For all $a,b \in \reals$ such that $a < b$ we have there exists $c \in \reals$ such that $a < c < b$.
\end{lemma}

\begin{lemma}\label{epsball_equal_openinterval}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$.
    Then $\epsBall{x}{\epsilon} = \intervalopen{x - \epsilon}{x + \epsilon}$.
\end{lemma}

\begin{lemma}\label{minus_behavior1}
    For all $x \in \reals$ we have $x - x = \zero$.
\end{lemma}

\begin{lemma}\label{minus_behavior2}
    For all $x \in \reals$ we have $x + \neg{x} = \zero$.
\end{lemma}

\begin{lemma}\label{minus_behavior3}
    For all $x \in \reals$ we have $\neg{x} = \zero - x$.
\end{lemma}

\begin{lemma}\label{reals_order_is_addition_with_positiv_number}
    For all $x,y \in \reals$ such that $x < y$ we have there exists $z \in \realsplus$ such that $x + z = y$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{reals_order_is_transitive}
    For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{reals_order_plus_minus}
    Suppose $a,b \in \reals$.
    Suppose $\zero < b$.
    Then $(a-b) < (a+b)$.
\end{lemma}
\begin{proof}
    We show that $a < (a+b)$.
    \begin{subproof}
        Trivial.
    \end{subproof}
    We show that $(a-b) < a$.
    \begin{subproof}
        Trivial.
    \end{subproof}
\end{proof}

\begin{lemma}\label{epsball_are_connected_in_reals}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$.
    Then for all $c \in \reals$ such that $(x - \epsilon) < c < (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
\end{lemma}
\begin{proof}
    $x - \epsilon \in \reals$.
    $x + \epsilon \in \reals$.


    It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
    Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$.
    $(x - \epsilon) < c < (x + \epsilon)$.
\end{proof}

\begin{theorem}\label{topological_basis_reals_is_prebasis}
    $\topoBasisReals$ is a topological prebasis for $\reals$.
\end{theorem}
\begin{proof}
    We show that $\unions{\topoBasisReals} \subseteq \reals$.
    \begin{subproof}
        It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$.
        Fix $x \in \unions{\topoBasisReals}$.
        \begin{byCase}
            \caseOf{$x = \emptyset$.}
                Trivial.
            \caseOf{$x \neq \emptyset$.}
                %There exists $U \in \topoBasisReals$ such that $x \in U$.
                Take $U \in \topoBasisReals$ such that $x \in U$.
                Follows by \cref{epsball_are_subseteq_reals_set,topological_basis_reals_eps_ball,epsilon_ball,minus,subseteq}.
        \end{byCase}
    \end{subproof}
    We show that $\reals \subseteq \unions{\topoBasisReals}$.
    \begin{subproof}
        It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
        Fix $x \in \reals$.
        $\epsBall{x}{1} \in \topoBasisReals$.
        Therefore $x \in \unions{\topoBasisReals}$ by \cref{one_in_reals,reals_one_bigger_zero,unions_intro,realsplus,plus_one_order,reals_order_minus_positiv,epsball_are_connected_in_reals}.
    \end{subproof}
\end{proof}

%\begin{lemma}\label{intervl_intersection_is_interval}
%    Suppose $a,b,a',b' \in \reals$.
%    Suppose there exist $x \in \reals$ such that $x \in \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
%    Then there exists $q,p \in \reals$ such that $q < p$ and $\intervalopen{q}{p} \subseteq \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
%\end{lemma}
%

\begin{lemma}\label{reals_order_total}
    For all $x,y \in \reals$ we have either $x < y$ or $x \geq y$. 
\end{lemma}
\begin{proof}
    It suffices to show that for all $x \in \reals$ we have for all $y \in \reals$ we have either $x < y$ or $x \geq y$. 
    Fix $x \in \reals$.
    Fix $y \in \reals$.
    Omitted.
\end{proof}

\begin{lemma}\label{topo_basis_reals_eps_iff}
    $X \in \topoBasisReals$ iff there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} = X$.
\end{lemma}

\begin{lemma}\label{topo_basis_reals_intro}
For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have $\epsBall{x}{\delta} \in \topoBasisReals$.
\end{lemma}

\begin{lemma}\label{realsplus_in_reals_plus}
    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$.
\end{lemma}

\begin{lemma}\label{realspuls_in_reals_minus}
    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x - y \in \reals$.
\end{lemma}

\begin{lemma}\label{eps_ball_implies_open_interval}
    Suppose $x \in \reals$.
    Suppose $\epsilon \in \realsplus$. 
    Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
\end{lemma}

\begin{lemma}\label{reals_existence_addition_reverse}
    For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
\end{lemma}
\begin{proof}
    Fix $\delta \in \reals$.
    Follows by \cref{reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
\end{proof}

\begin{lemma}\label{reals_addition_minus_behavior1}
    For all $a,b,c \in \reals$ such that $a = b + c$ we have $b = a - c$.
\end{lemma}
\begin{proof}
    It suffices to show that for all $a \in \reals$ for all $b \in \reals$ for all $c \in \reals$ if $a = b + c$ then $b = a - c$.
    Fix $a \in \reals$.
    Fix $b \in \reals$.
    Fix $c \in \reals$.
    Suppose $a = b + c$.
    Then $a + \neg{c} = b + c + \neg{c}$.
    Therefore $a - c = b + c + \neg{c}$.
    $a - c = (b + c) - c$.
    $(b + c) - c = (b + c) + \neg{c}$.
    $(b + c) + \neg{c} = b + (c + \neg{c})$.
    $b + (c + \neg{c}) = b + (\zero)$.
    $a - c = b$.
\end{proof}

\begin{lemma}\label{reals_addition_minus_behavior2}
    For all $a,b,c \in \reals$ such that $a = b - c$ we have $b = c + a$.
\end{lemma}

\begin{lemma}\label{open_interval_eq_eps_ball}
    Suppose $a,b \in \reals$.
    Suppose $a < b$.
    Then there exist $x,\epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
\end{lemma}
\begin{proof}
    Let $\delta = (b-a)$.
    $\delta$ is positiv by \cref{minus_in_reals,minus_behavior3,reals_axiom_zero_in_reals,reals_order_behavior_with_addition,minus_behavior1,minus}.
    There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
    Let $x = a + \epsilon$.
    $a + \delta = b$.
    $a + \epsilon + \epsilon = b$. 
    $x + \epsilon = b$.
    $\epsilon \in \realsplus$ by \cref{reals_order_behavior_with_addition,reals_axiom_kommu,reals_axiom_zero,reals_order_is_transitive,reals_add,minus_behavior1,minus_behavior3,minus,reals_order_total,reals_axiom_zero_in_reals,realsplus}.
    $a = x - \epsilon$.
    $b = x + \epsilon$.
    We show that $\intervalopen{a}{b} \subseteq \epsBall{x}{\epsilon}$.
    \begin{subproof}
        It suffices to show that for all $y \in \intervalopen{a}{b}$ we have $y \in \epsBall{x}{\epsilon}$.
        Fix $y \in \intervalopen{a}{b}$.
    \end{subproof}
    We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$.
    \begin{subproof}
        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$.
        Fix $y \in \epsBall{x}{\epsilon}$.
    \end{subproof}

\end{proof}

\begin{lemma}\label{intersection_openinterval_inclusion_of_border}
    Suppose $a,b,x,y \in \reals$.
    Suppose $a < b$.
    Suppose $x < y$.
    If $a \leq x < y \leq b$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{intersection_openinterval_lower_border_eq}
    Suppose $a,b,x,y \in \reals$.
    Suppose $a < b$.
    Suppose $x < y$.
    If $a = x$ and $b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{intersection_openinterval_upper_border_eq}
    Suppose $a,b,x,y \in \reals$.
    Suppose $a < b$.
    Suppose $x < y$.
    If $a \leq x$ and $b = y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{intersection_openinterval_none_border_eq}
    Suppose $a,b,x,y \in \reals$.
    Suppose $a < b$.
    Suppose $x < y$.
    If $a \leq x < b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{b}$.
\end{lemma}
\begin{proof}
    Omitted.
\end{proof}

\begin{lemma}\label{reals_order_total2}
    For all $a,b \in \reals$ we have $a < b \lor a > b \lor a = b$.
\end{lemma}


\begin{theorem}\label{topological_basis_reals_is_basis}
    $\topoBasisReals$ is a topological basis for $\reals$.
\end{theorem}
\begin{proof}
    $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}.
    Let $B = \topoBasisReals$.
    It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
    Fix $U \in B$.
    Fix $V \in B$.
    It suffices to show that for all $x \in U \inter V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
    Fix $x \in U \inter V$.
    \begin{byCase}
        \caseOf{$U \inter V = \emptyset$.}
            Trivial.
        \caseOf{$U \inter V \neq \emptyset$.}
            Then $U \inter V$ is inhabited.
            $x \in \reals$ by \cref{inter_lower_left,subseteq,topological_prebasis_iff_covering_family,omega_is_an_ordinal,naturals_subseteq_reals,subset_transitive,suc_subseteq_elim,ordinal_suc_subseteq}.
            There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
            There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
            Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
            Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
            Let $a = (x_1 - \alpha)$.
            Let $b = (x_1 + \alpha)$.
            Let $c = (x_2 - \beta)$.
            Let $d = (x_2 + \beta)$.
            We have $a < b$ and $a < x$ and $x < b$.
            We have $c < d$ and $c < x$ and $x < d$.
            We have $a \in \reals$.
            We have $b \in \reals$.
            We have $c \in \reals$.
            We have $d \in \reals$.
            We show that there exist $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$.
            \begin{subproof} 
                \begin{byCase}
                    \caseOf{$a < c$.}
                        \begin{byCase}
                            \caseOf{$b < d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
                            \caseOf{$b = d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
                            \caseOf{$b > d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
                        \end{byCase}
                    \caseOf{$a = c$.}
                        \begin{byCase}
                            \caseOf{$b < d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
                            \caseOf{$b = d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
                            \caseOf{$b > d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
                        \end{byCase}
                    \caseOf{$a > c$.}
                        \begin{byCase}
                            \caseOf{$b < d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
                            \caseOf{$b = d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
                            \caseOf{$b > d$.}
                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
                        \end{byCase}
                \end{byCase}
            \end{subproof}

            Take $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$.
            We have $a',b' \in \reals$ by assumption.
            We have $a' < b'$ by \cref{id_img,epsilon_ball,minus,intervalopen,reals_order_is_transitive}.
            Then there exist $x',\epsilon'$ such that $x' \in \reals$ and $\epsilon' \in \realsplus$ and $\intervalopen{a'}{b'} = \epsBall{x'}{\epsilon'}$.
            Then $x \in \epsBall{x'}{\epsilon'}$.

            Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}.
            %Then $(x_1 - \alpha) < (x_2 + \beta)$.

            %Therefore $U \inter V = \intervalopen{}{(x_2 + \beta)}$.

            %We show that if there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$ then there exists $W\in B$ such that $x\in W\subseteq U, V$.
            %\begin{subproof}
            %    Suppose there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
            %    $x \in \epsBall{x}{\delta}$.
            %    $\epsBall{x}{\delta} \subseteq U$.
            %    $\epsBall{x}{\delta} \subseteq V$.
            %    $\epsBall{x}{\delta} \in B$.
            %\end{subproof}
            %It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.


            %It suffices to show that there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} \subseteq u \inter V$.
            %There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
            %There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
            %Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
            %Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
            %\begin{byCase}
            %    \caseOf{$x_1 = x_2$.}
            %        Take $\gamma \in \realsplus$ such that either $\gamma = \alpha \land \gamma \leq \beta$ or $\gamma \leq \alpha \land \gamma = \beta$.
            %    \caseOf{$x_1 < x_2$.}
            %    \caseOf{$x_1 > x_2$.}
            %\end{byCase}
            %%Take $m$ such that $m \in \min{\{(x_1 + \alpha), (x_2 + \beta)\}}$.
            %Take $n$ such that $n \in \max{\{(x_1 - \alpha), (x_2 - \beta)\}}$.
            %Then $m < x < n$.
            %We show that there exists $x_1 \in \reals$ such that $x_1 \in U \inter V$ and $x_1 < x$.
            %\begin{subproof}
            %    Suppose not.
            %    Then For all $y \in U \inter V$ we have $x \leq y$.
            %\end{subproof}
            %We show that there exists $x_2 \in \reals$ such that $x_2 \in U \inter V$ and $x_2 > x$.
            %\begin{subproof}
            %    Trivial.
            %\end{subproof}
    \end{byCase}
\end{proof}

\begin{axiom}\label{topological_space_reals}
    $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
\end{axiom}

\begin{theorem}\label{reals_is_topological_space}
    $\reals$ is a topological space.
\end{theorem}
\begin{proof}
    $\topoBasisReals$ is a topological basis for $\reals$.
    Let $B = \topoBasisReals$.
    We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$.
    \begin{subproof}
        It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$.
        Fix $A \in \opens[\reals]$.
        Follows by \cref{powerset_elim,topological_space_reals,genopens}.
    \end{subproof}
    We show that $\reals \in\opens[\reals]$.
    \begin{subproof}
        $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
        $\unions{B} \in \genOpens{B}{\reals}$.
        $\reals \subseteq \unions{B}$.
    \end{subproof}
    We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$.
    \begin{subproof}
        Follows by \cref{topological_space_reals,inters_in_genopens}.
    \end{subproof}
    We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$.
    \begin{subproof}
        Follows by \cref{topological_space_reals,union_in_genopens}.
    \end{subproof}
    $\carrier[\reals] = \reals$.
    Follows by \cref{topological_space}.
\end{proof}

\begin{proposition}\label{open_interval_is_open}
    Suppose $a,b \in \reals$.
    Then $\intervalopen{a}{b} \in \opens[\reals]$.
\end{proposition}