\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{locale of real numbers}

\hypertarget{the_locale_of_real_numbers}{}\section*{{The locale of real numbers}}\label{the_locale_of_real_numbers}

\noindent\hyperlink{summary}{Summary}\dotfill \pageref*{summary} \linebreak
\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{opens}{Opens}\dotfill \pageref*{opens} \linebreak
\noindent\hyperlink{the_zigzag_lemma}{The zigzag lemma}\dotfill \pageref*{the_zigzag_lemma} \linebreak
\noindent\hyperlink{the_frame_of_opens}{The frame of opens}\dotfill \pageref*{the_frame_of_opens} \linebreak
\noindent\hyperlink{open_intervals_as_opens}{Open intervals as opens}\dotfill \pageref*{open_intervals_as_opens} \linebreak
\noindent\hyperlink{open_sets_closed_sets_and_points}{Open sets, closed sets, and points}\dotfill \pageref*{open_sets_closed_sets_and_points} \linebreak
\noindent\hyperlink{the_heineborel_theorem}{The Heine--Borel theorem}\dotfill \pageref*{the_heineborel_theorem} \linebreak


\hypertarget{summary}{}\subsection*{{Summary}}\label{summary}

This page gives an elementary description of the [[locale]] of [[real numbers]], that is the localic [[real line]]. The development is manifestly [[constructive mathematics|constructive]] and even [[predicative mathematics|predicative]] over the [[natural numbers]] (although we are somewhat careless with the language and do not always point out when a set may predicatively be a [[proper class]]). Ideally, we will show that our construction satisfies the seven `headline properties' of the real line described by \href{http://www.paultaylor.eu/ASD/dedras/intro}{Bauer \& Taylor} (although so far we cover only the Heine--Borel theorem).

The exposition here is pretty much [[Toby Bartels|my]] own work, although of course the basic ideas are well known to many. In particular, the technical zigzag lemma is mine (but it is not a very deep result!).

\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

To describe the locale of the real numbers, we need first of all to describe what an open in the real line is. The key insight is that an open set is determined by the open intervals of [[rational numbers]] that it contains. This is analogous to the key insight of [[Richard Dedekind]]'s definition of [[real number]]: that a point in the real line is determined by which open intervals of rational numbers that it belongs to. (Once you're talking about rational numbers, things are manageable.)

\hypertarget{opens}{}\subsection*{{Opens}}\label{opens}

An \textbf{open} in the real line is a [[binary relation]] ${\sim}$ on the [[rational numbers]] that satisfies the four properties listed below. Intuitively, we have $a \sim b$ iff the open [[interval]] $(a,b)$ is contained in the corresponding [[open subspace|open set]].

\begin{enumerate}%
\item If $a \geq b$, then $a \sim b$.
\item If $a \geq b \sim c \geq d$, then $a \sim d$.
\item If $a \sim b \gt c \sim d$, then $a \sim d$.
\item If $b \sim c$ whenever $a \lt b$ and $c \lt d$, then $a \sim d$.

\end{enumerate}
If we suggestively formally write $(a, b) \subseteq U_\sim$ for $a \sim b$, and $(a, b) \subseteq (c, d)$ for $c \leq a$ and $b \leq d$, then these say

\begin{enumerate}%
\item If $a \geq b$, then $(a, b) \subseteq U_\sim$.
\item If $(a, d) \subseteq (b, c)$ and $(b, c) \subseteq U_\sim$, then $(a, d) \subseteq U_\sim$.
\item If $c \lt b$ and $(a, b), (c, d) \subseteq U_\sim$, then $(a, d) \subseteq U_\sim$.
\item If $(b, c) \subseteq U_\sim$ for all $(b, c) \subsetneq (a, d)$, then $(a, d) \subseteq U_\sim$.

\end{enumerate}
Property (1) is motivated because $(a,b)$ is [[empty subset|empty]] whenever $a \geq b$. Property (2) is motivated because inclusion is transitive. Property (3) is motivated because if $c \lt b$, then $(a, d) = (a, b) \cup (c, d)$. Property (4) is motivated because $\bigcup_{(b, c) \subsetneq (a, d)} (b, c) = (a, d)$.

The really interesting property is property (3). It in fact generalises as follows:

\begin{itemize}%
\item If\begin{equation}
a_1 \sim b_1 \gt a_2 \sim b_2 \gt \cdots \gt a_n \sim b_n
,
\label{zigzag}\end{equation}
then $a_1 \sim b_n$.



\end{itemize}
We call the combined hypothesis of this property a \textbf{zigzag}; each hypothesis $a_i \sim b_i$ is a \textbf{zig}, and each hypothesis $b_i \gt a_{i^+}$ is a \textbf{zag}. To indicate the length of a zigzag, we will count the zigs; the zigzag \eqref{zigzag} has $n$ zigs (and $n - 1$ zags). A typical nondegenerate zigzag with $3$ zigs is shown below; it consists of $3$ overlapping open intervals, each of which belongs to a given open set; we are motivated to conclude that the entire interval from $a_1$ to $b_3$ belongs to that open set.

[[!include zigzag of real numbers - SVG]]

Thus the zigzag property for $n = 2$ is property (3), the zigzag property for $n = 1$ is trivial (if $a \sim b$, then $a \sim b$), and the zigzag property for $n \gt 2$ may be proved by [[induction]]. (There is also a sense in which the zigzag property for $n = 0$ is property (1), but I haven't quite got my head around that. It would be awesome if the zigzag property for $n = \infty$ could be interepreted as property (4), but that seems unlikely so far.)

If $G$ is an open in the real line, then we write $(a,b) \subseteq G$ to mean that $a$ is related to $b$ through $G$ and say that $G$ \textbf{contains} the interval from $a$ to $b$.

\hypertarget{the_zigzag_lemma}{}\subsection*{{The zigzag lemma}}\label{the_zigzag_lemma}

We will often have occasion to consider a zigzag as in \eqref{zigzag}, but where the various zigs are taken relative to different opens. Nevertheless, we will usually want to say something about the relationship of $a_1$ to $b_n$, and it will often be convenient to assume, for all $i$, that $a_1 \leq a_i$ and $b_i \leq b_n$. We may do so without loss of generality as follows: consider the smallest value of $i$ such that $b_i \geq b_n$, truncate the zigzag so that it now has only $i$ zigs, and change the new endpoint $b_i$ to the old endpoint $b_n$. The final zig $(a_i,b_i) \subseteq G_i$ becomes $(a_i,b_n) \subseteq G_i$, which will hold by property (2) since $b_i \geq b_n$. Now consider the largest value of $j \leq i$ such that $a_1 \geq a_j$, and truncate similarly on the other side. We now have a zigzag with $i - j + 1$ zigs that never falls below $a_1$ on a zag nor rises above $b_n$ on a zig.

To be precise:

\begin{ulemma}
Given a collection $\mathcal{C}$ of opens and a zigzag in which each zig holds relative to some open in $\mathcal{C}$, there exists a zigzag \eqref{zigzag} in which each zig holds relative to some open in $\mathcal{C}$, $a_1 \leq a_i$ for each $i$, and $b_i \leq b_n$ for each $i$.

(Since each $b_i \gt a_{i^+}$, it follows further that $a_i \lt b_n$ for each $i \gt 1$ and $a_1 \lt b_i$ for each $i \lt n$, although this corollary doesn't seem to be particularly useful.)

\end{ulemma}
At the moment, this lemma is used only in the proof of the infinite distributivity law.

\hypertarget{the_frame_of_opens}{}\subsection*{{The frame of opens}}\label{the_frame_of_opens}

The opens form a [[subobject|sub]]-[[poset]] of the [[power set]] $\mathcal{P}(\mathbb{Q} \times \mathbb{Q})$. This poset is in fact a [[frame]], as we will now show. (It is \emph{not} a subframe of the power set, since the [[joins]] are different. It \emph{is} a sub-[[inflattice]] of the power set, although this seems to be a red herring at least for infinitary [[meets]], since those are not part of the frame structure that we need.)

The [[top element|top]] open, denoted $\mathbb{R}$, is the binary relation which is always true. Given two opens $G$ and $H$, their [[meet]] in the poset of opens, denoted $G \cap H$, is simply their [[logical conjunction|conjunction]], that is their [[intersection]] as [[subsets]] of $\mathbb{Q} \times \mathbb{Q}$. (In fact, given any collection of opens, their meet is their conjunction.) It is straightforward to check that $\mathbb{R}$ and $G \cap H$ are opens and to prove that these are the desired meets. Intuitively, this all works because an open interval will be contained in the intersection of a family of open sets if and only if it is contained in each individual open set.

The [[bottom element|bottom]] open, denoted $\empty$, is the binary relation $\geq$. That is, $(a,b) \subseteq \empty$ iff $a \geq b$. It is easy to check that this is an open; it precedes every open by property (1). Intuitively, this corresponds to the [[empty subset]] of the real line; $(a,b)$ is empty if and only if $a \geq b$. However, note that $\empty$ is \emph{not} the empty subset of $\mathbb{Q} \times \mathbb{Q}$; the notation follows our topological intuition rather than the [[relation theory|algebra of relations]].

Given two opens $G$ and $H$, their [[join]] in the poset of opens, denoted $G \cup H$, is defined as follows: $(a,b) \subseteq G \cup H$ if and only if there exists a zigzag \eqref{zigzag} with $a = a_1$ and $b = b_n$ in which each zig is of the form $(a_i,b_i) \subseteq G$ or $(a_i,b_i) \subseteq H$. It is immediate that this is an open in which $G$ and $H$ are both contained. Conversely, any open in which $G$ and $H$ are contained must contain this open $G \cup H$, by property (3).

More generally, given any family $(G_k)_k$ of opens, their [[join]] in the poset of opens, denoted $\bigcup_k G_k$, is defined as follows: $(a,b) \subseteq \bigcup_k G_k$ if and only if $a \geq b$ or there exists a zigzag \eqref{zigzag} with $a = a_1$ and $b = b_n$ in which each zig is of the form $(a_i,b_i) \subseteq G_k$ for some $k$. (We can leave out the $a \geq b$ clause if the family is [[inhabited set|inhabited]].) The same argument applies as before. Note that each individual zigzag has finitely many zigs, and therefore involves finitely many of the opens $G_k$, even when taking the join of an infinite family.

Finally, we must check the distributive law $G \cap \bigcup_k H_k \subseteq \bigcup_k (G \cap H_k)$. That is, if $a \sim b$ directly through $G$ and $a \sim b$ through a zigzag of $H$s (or $a \geq b$), then we need that $a \sim b$ through a zigzag in which each zig is related both through $G$ and through some $H$ (or $a \geq b$). To prove this (ignoring the trivial case where $a \geq b$), start with the zigzag of $H$s, and apply the zigzag lemma to get a zigzag of $H$s in which each zig involves values bounded by $a$ and $b$. Then these zigs hold for $G$ as well, by property (2). Therefore, we may interpret each zig using $G \cap H_k$ for some $k$, proving the desired result.

This frame of opens, interpreted as a [[locale]], is \textbf{the locale of real numbers}. As usual, we denote this locale with the same symbol as the top element of its frame, in this case $\mathbb{R}$. (Of course, the true etymology of the symbols runs in the other order.)

\hypertarget{open_intervals_as_opens}{}\subsection*{{Open intervals as opens}}\label{open_intervals_as_opens}

Given rational numbers $a$ and $b$, the open interval $(a,b)$ may itself be interpreted as an open in the real line, also denoted $(a,b)$, as follows: let $(c,d) \subseteq (a,b)$ hold if every rational number strictly between $c$ and $d$ (in that order) is also strictly between $a$ and $b$ (in that order). In other words, we interpret `${\subseteq}$' literally as comparing subsets of $\mathbb{Q}$. It is straightforward to check that this condition does indeed define an open. There is now a third way to interpret `$(c,d) \subseteq (a,b)$'; interpreting both intervals as opens in the real line, this states that the first is contained in the second. But again, it is easy to check that this is equivalent; $(c,d) \subseteq (a,b)$ (in the set-theoretic sense) if and only if $(e,f) \subseteq (a,b)$ whenever $(e,f) \subseteq (c,d)$. Notice that $(a,b) = \empty$ whenever $a \geq b$.

We can actually generalise this somewhat. Given any set $L$ of rational numbers and any set $U$ of rational numbers, we may define the open $(\inf U, \sup L)$ as follows: let $(a,b) \subseteq (\inf U, \sup L)$ hold if every rational number strictly between $a$ and $b$ (in that order) is greater than some element of $U$ and less than some element of $L$. If the [[infimum]] of $U$ and the [[supremum]] of $L$ exist in the usual sense as rational numbers, then this agrees with the previous paragraph. If instead $U$ or $L$ is the set of all rational numbers, then we write $-\infty$ for $\inf U$ or $\infty$ for $\sup L$. In general, we may interpret $\inf U$ as an [[extended real number|extended]] [[upper real number|upper real]] and $\sup L$ as an extended [[lower real number|lower real]]. Classically, every extended upper or lower real is either a real number, $-\infty$, or $\infty$; only the converse holds constructively. Notice that $(-\infty,\infty) = \mathbb{R}$.

Since we will refer to them below, we will state for the record the complete definitions of $(-\infty,a)$ and $(a,\infty)$ for a rational number $a$. We have $(b,c) \subseteq (-\infty,a)$ iff every rational number strictly between $b$ and $c$ is less than $a$, that is iff $b \geq c$ or $c \leq a$. Similarly, we have $(b,c) \subseteq (a,\infty)$ iff every rational number strictly between $b$ and $c$ is greater than $a$, that is iff $b \geq c$ or $b \geq a$. A fortiori, $(b,c) \subseteq (-\infty,0)$ if $c = 0$, and $(b,c) \subseteq (1, \infty)$ if $b = 1$.

\hypertarget{open_sets_closed_sets_and_points}{}\subsection*{{Open sets, closed sets, and points}}\label{open_sets_closed_sets_and_points}

We think of each open as defining an [[open subspace|open subset]] of the real line, but we can equally well think of it as defining a [[closed subspace|closed subset]]. The difference between these perspectives is reflected in [[complement]]ary criteria for when a real number belongs to the set. So to make sense of this, we must identify the [[point|points]] of the real line.

Recall that a [[real number]] may be defined as a pair $(L,U)$ of [[inhabited set|inhabited]] [[subsets]] of $\mathbb{Q}$ satisfying the following properties:

\begin{enumerate}%
\item If $a \in L$, then $a \lt b$ for some $b \in L$.
\item If $b \in U$, then $a \lt b$ for some $a \in U$.
\item If $a \in L$ and $b \in U$, then $a \lt b$.
\item If $a \lt b$, then $a \in L$ or $b \in U$.

\end{enumerate}
We define a \textbf{point} of the real line to be a real number in this sense. Given such a point $x = (L,U)$ and a rational number $a$, we write $a \lt x$ to mean that $a \in L$ and $a \gt x$ to mean that $a \in U$. If we wish to refer to $L$ and $U$ directly, we may call $L$ the \textbf{lower set} of $x$ and $U$ the \textbf{upper set}.

Given a point $x$ and an open $G$, we say that $x$ \textbf{belongs} to $G$, written $x \in G$, if $(a,b) \subseteq G$ for some $a \lt x$ and $b \gt x$; that is, $G$ contains an interval from some element of the lower set to some element of the upper set of $x$. We have $x \in \mathbb{R}$ since its lower and upper sets are inhabited. If $x \in G$ and $x \in H$, with $(a,b) \subseteq G$ and $(c,d) \subseteq H$, then $\big(\max(a,c), \min(b,d)\big) \subseteq G \cap H$, so $x \in G \cap H$; note that this argument fails for infinitary intersections. (The converse, that $x \in G$ and $x \in H$ if $x \in G \cap H$, is immediate.) Dually, suppose that $x \in \bigcup_k G_k$, as shown by some zigzag (since $a \geq b$ is impossible when $a \lt x$ and $b \gt x$, by 3). Applying condition (4) of the definition of real number to each zag, we have $a_{i^+} \lt x$ or $b_i \gt x$, for each $i \lt n$. Checking all $2^{n-1}$ possibilities, and knowing that $a_1 \lt x$ and $b_n \gt x$ in any case, we must have $a_i \lt x$ and $b_i \gt x$ for some $i$. Then we have $x \in G_k$ for some $k$, whichever corresponds to the $i$th zig. (The converse, that $x \in \bigcup_k G_k$ if $x \in G_k$ for some $k$, is immediate.)

Therefore, each point defines a [[completely prime filter]] on the frame of all opens, which is the definition of a [[point of a locale|point]] in general locale theory. Conversely, given such a completely prime filter $P$, let $L$ be the set of all rational numbers $a$ such that the open interval $(a, \infty)$ (when interpreted as an open in the real line as defined above) is in $P$, and symmetrically let $U$ be the set of all $a$ such that $(-\infty, a) \in P$.

Given a point $x$ and an open $G$, we say that $x$ \textbf{co-belongs} to $G$, written $x \notin G$, if we never have $a \lt x$, $b \gt x$, and $(a,b) \subseteq G$, which is precisely the [[negation]] of the property that $x \in G$. We think of this condition as defining a \emph{[[closed subspace|closed]]} set to which $x$ \emph{does} belong. Notice that $x \notin \bigcup_k G_k$ if and only if $x \notin G_k$ for each $k$, giving the desired behaviour for an arbitrary intersection of closed sets (which corresponds to union of open sets under [[de Morgan duality]]). We also have that $x \notin \mathbb{R}$ always fails, and $x \notin G \cap H$ if $x \notin G$ or $x \notin H$. To prove that $x \notin G$ or $x \notin H$ whenever $x \notin G \cap H$, however, we must use [[excluded middle]]; constructively, closed sets don't behave well under union.

A related question is whether we can reconstruct $G$ from the set of points which belong to it. This should be equivalent to the [[fan theorem]], which is classically true and also accepted by [[Jan Brouwer|Brouwer]]'s school of intuitionism, but refuted in the Russian school in which all real numbers are assumed to be [[computable number|computable]]. (I should check this.) Arguably, the real lesson of these logical technicalities is that we should remember that opens, not points, are the fundamental concept in a locale.

\hypertarget{the_heineborel_theorem}{}\subsection*{{The Heine--Borel theorem}}\label{the_heineborel_theorem}

The classical [[Heine-Borel theorem|Heine–Borel theorem]], as a statement about sets of real numbers, may fail constructively; this is related to the comments above about the [[fan theorem]]. But the beauty of the localic approach is that Heine--Borel necessarily holds when interpreted as a statement about opens in the locale of real numbers. To state the theorem, we must define what it means for a collection of opens to [[cover]] the [[unit interval]]. We will give an ad-hoc definition, but this may also be derived from the general theory of [[closed sublocale]]s which allows us to interpret the unit interval as a [[compact space|compact]] locale in its own right.

\begin{udefn}
An \textbf{[[open cover]] of the unit interval} is a collection $\mathcal{C}$ of opens in the real line such that $\mathbb{R}$ is the join of $(-\infty,0)$, $(1,\infty)$, and the elements of $\mathcal{C}$.

\end{udefn}
\begin{utheorem}
(Heine--Borel)

Every open cover of the unit interval has a finite subcover.

\end{utheorem}
\begin{proof}
The proof is almost embarrassingly simple. The key point is that the construction of joins in terms of zigzags involves only finite zigzags, even for an infinitary join.

Let $J$ be the join of $(-\infty,0)$, $(1,\infty)$, and the elements of $\mathcal{C}$. If this equals $\mathbb{R}$, then in particular $(-1,2) \subseteq J$, a fact which is given by some zigzag $\zeta$. This zigzag involves only finitely many of the elements of $\mathcal{C}$; let $\mathcal{D}$ be the collection of these, and let $K$ be the join of $(-\infty,0)$, $(1,\infty)$, and $\mathcal{D}$. Now if $(a,b)$ is any pair of rational numbers, we construct a zigzag showing that $(a,b) \subseteq K$ as follows: the zig $(a,0) \subseteq (-\infty,0)$, the zag $0 \gt -1$, the zigzag $\zeta$ from $-1$ to $2$, the zag $2 \gt 1$, and the zig $(1,b) \subseteq (1,\infty)$. This is always a valid zigzag, so $K = \mathbb{R}$. Therefore, the finite collection $\mathcal{D}$ covers the unit interval.

\end{proof}
This proof generalises immediately to any closed interval $[a,b]$, for $a$ any upper real and $b$ any lower real. But note that we do not say `extended' here; we need to find some rational number (analogous to $-1$ in the proof above) smaller than $a$ and some rational number (analogous to $2$ above) larger than $b$. So the Heine--Borel theorem applies only to \emph{bounded} closed intervals.

[[!redirects the locale of real numbers]] [[!redirects locale of real numbers]] [[!redirects localic real numbers]] [[!redirects localic real number]] [[!redirects the localic real line]] [[!redirects localic real line]]



\end{document}