\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*{one-sided real number}

\hypertarget{onesided_real_numbers}{}\section*{{One-sided real numbers}}\label{onesided_real_numbers}

\noindent\hyperlink{summary}{Summary}\dotfill \pageref*{summary} \linebreak
\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{lower_reals}{Lower reals}\dotfill \pageref*{lower_reals} \linebreak
\noindent\hyperlink{upper_reals}{Upper reals}\dotfill \pageref*{upper_reals} \linebreak
\noindent\hyperlink{order_relations}{Order relations}\dotfill \pageref*{order_relations} \linebreak
\noindent\hyperlink{suprema_and_infima}{Suprema and infima}\dotfill \pageref*{suprema_and_infima} \linebreak
\noindent\hyperlink{arithmetic}{Arithmetic}\dotfill \pageref*{arithmetic} \linebreak
\noindent\hyperlink{topology}{Topology}\dotfill \pageref*{topology} \linebreak
\noindent\hyperlink{in_topos_theory}{In topos theory}\dotfill \pageref*{in_topos_theory} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

There are really two notions of one-sided real number: lower reals and upper reals. But there is a nearly perfect symmetry between them (although the lower reals seem to get slightly more use).

These are largely concepts in [[constructive mathematics]]. Using [[excluded middle]], a bounded one-sided real number is simply a [[real number]], but constructively they are more general (and less well behaved). Lower reals are particularly important in constructive [[measure theory]] as the values taken by [[positive measures]] (and more generally are used to define [[extended positive cones]]).

However, even in [[classical mathematics]], there are some differences, at least in emphasis and application. First, it is most natural to include $\infty$ as a lower real and include $-\infty$ as an upper real. (However, you can restrict to \emph{bounded} lower/upper reals to avoid that, or alternatively genralise to \emph{extended} lower/upper reals if you want to include both $\pm\infty$ at once.) Also, the natural [[topological structure|topology]] on the lower reals is the \emph{lower [[semicontinuous topology]]} (and the natural topology on the upper reals is the \emph{upper semicontinuous topology}).

One-sided numbers are sometimes called (upper or lower) \emph{semicontinuous} numbers. To see why, consider a [[locale]] (or [[topological space]]) $L$, and consider the (upper or lower) [[semicontinuous functions]] (real-valued) on $L$. On the one hand, these are the same as the [[continuous functions]] from $L$ to (classically) the set of real numbers equipped with the semicontinuous topology or to (constructively) a locale whose [[point of a locale|points]] are the one-sided real numbers. On the other hand, these semicontinuous functions are precisely the [[internal logic|internal]] one-sided real numbers in the [[topos of sheaves]] over $L$.

Lower and upper reals don't interact well together. Their ``intersection'' is the set of [[MacNeille real numbers]], which is moderately well-behaved; it also contains the set of [[located real numbers]], which is better-behaved algebraically (but not, constructively, a complete lattice). But it seems hard, constructively, to find any reasonably behaved notion of ``real number'' than contains both upper and lower reals.

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

(In the following, `number' without qualification may be taken to mean either a [[real number]] or a [[rational number]]; the result is the same either way. Indeed, we could take any [[dense subset|dense set]] of real numbers.)

A \textbf{lower real number} is the [[supremum]] of an [[inhabited set|inhabited]] set of numbers. A \textbf{bounded lower real} is the supremum of an inhabited set of numbers that has a finite upper bound. An \textbf{extended lower real} is the supremum of an arbitrary set of numbers.

An \textbf{upper real number} is the [[infimum]] of an inhabited set of numbers. A \textbf{bounded upper real} is the infimum of an inhabited set of numbers that has a finite lower bound. An \textbf{extended lower real} is the infimum of an arbitrary set of numbers.

We cannot generalize further by taking more extrema of the same sort. Explicitly, the supremum of any inhabited set of lower reals is a lower real and the infimum of any inhabited set of upper reals is an upper real. Similar results obtain if we use either bounded or extended reals, so long as we also either require the set to bounded or allow it to be [[empty subset|empty]].

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

There are some choices as to how exactly to represent one-sided real numbers; we will define them here as certain [[subsets]] of the set $\mathbb{Q}$ of [[rational numbers]]. If we replaced $\mathbb{Q}$ with any other [[dense subset]] of the [[real line]], then the definitions would end up being equivalent.

\hypertarget{lower_reals}{}\subsubsection*{{Lower reals}}\label{lower_reals}

An \textbf{extended lower real number} is any subset $L$ of $\mathbb{Q}$ such that

\begin{itemize}%
\item if $a \in L$, then $a \lt b$ for some $b \in L$; and
\item if $a \lt b$ and $b \in L$, then $a \in L$.

\end{itemize}
We can actually combine these into a single rule:

\begin{itemize}%
\item $a \in L$ if and only if $a \lt b$ for some $b \in L$.

\end{itemize}
A \textbf{lower real number} is an extended lower real $L$ such that:

\begin{itemize}%
\item some $a \in L$.

\end{itemize}
A \textbf{bounded lower real number} is a lower real $L$ such that

\begin{itemize}%
\item some $b \notin L$.

\end{itemize}
When treated explicitly as a subset of $\mathbb{Q}$, we call $L$ a \textbf{[[lower set]]}. When we interpret $L$ as a one-sided real number $x$, we write $a \lt x$ to mean that $a \in L$. Conversely, we can interpret any rational number, or even any real number, $x$ as a bounded lower real, specifically as the set of all rational numbers less than $x$. (A bounded lower real is \textbf{located} if it is the lower real obtained in this way from a real number; classically, every bounded lower real number is located.) We interpret $\infty$ as the lower real whose lower set is all of $\mathbb{Q}$; we interpret $-\infty$ as the extended lower real whose lower set is empty.

\hypertarget{upper_reals}{}\subsubsection*{{Upper reals}}\label{upper_reals}

An \textbf{extended upper real number} is any subset $U$ of $\mathbb{Q}$ such that

\begin{itemize}%
\item if $b \in U$, then $a \lt b$ for some $a \in U$; and
\item if $a \lt b$ and $a \in U$, then $b \in U$.

\end{itemize}
We can actually combine these into a single rule:

\begin{itemize}%
\item $b \in U$ if and only if $a \lt b$ for some $a \in U$.

\end{itemize}
An \textbf{upper real number} is an extended upper real $U$ such that:

\begin{itemize}%
\item some $b \in U$.

\end{itemize}
A \textbf{bounded upper real number} is an upper real $U$ such that

\begin{itemize}%
\item some $a \notin U$.

\end{itemize}
When treated explicitly as a subset of $\mathbb{Q}$, we call $U$ an \textbf{[[upper set]]}. When we interpret $U$ as a one-sided real number $x$, we write $x \lt b$ to mean that $b \in U$. Conversely, we can interpret any rational number, or even any real number, $x$ as a bounded upper real, specifically as the set of all rational numbers greater than $x$. (A bounded upper real is \textbf{located} if it is the upper real obtained in this way from a real number; classically, every bounded upper real number is located.) We interpret $-\infty$ as the upper real whose upper set is all of $\mathbb{Q}$; we interpret $\infty$ as the extended upper real whose upper set is empty.

\hypertarget{order_relations}{}\subsection*{{Order relations}}\label{order_relations}

We define [[order]] relations between extended lower reals $x$ and $y$ as follows:

\begin{itemize}%
\item $x \lt y$ if and only if there exists a rational number $a$ such that $a \lt y$ but not $a \lt x$;
\item $x \leq y$ if and only if $a \lt y$ for every rational number $a$ such that $a \lt x$.

\end{itemize}
In other words, $\leq$ is $\subseteq$ on lower sets, and $\lt$ is $\subsetneq$ (in an appropriate sense).

We define order relations between extended upper reals $x$ and $y$ as follows:

\begin{itemize}%
\item $x \lt y$ if and only if there exists a rational number $b$ such that $x \lt b$ but not $y \lt b$;
\item $x \leq y$ if and only if $x \lt b$ for every rational number $b$ such that $y \lt b$.

\end{itemize}
In other words, $\leq$ is $\supseteq$ on upper sets, and $\lt$ is $\supsetneq$.

We now have multiple meanings for $x \lt y$ or $x \leq y$ if one or both of these is already a rational number or a real number, but it is a theorem that the meanings are all consistent. We also have $-\infty \leq x \leq \infty$ for every extended number $x$, and $-\infty \lt x \lt \infty$ for every bounded number $x$. Finally, $x \leq y$ if $x \lt y$ or $x = y$; the converse holds classically.

Each version of $\leq$ is a [[partial order]] and each version of $\lt$ is a [[quasiorder]]. By [[excluded middle]], $\leq$ is a [[total order]] and $\lt$ is the corresponding [[linear order]], but neither of these results holds constructively. In particular, the [[comparison]] law for $\lt$ is invalid, which is why one-sided reals are not as well behaved as ordinary (located) [[real numbers]].

\hypertarget{suprema_and_infima}{}\subsection*{{Suprema and infima}}\label{suprema_and_infima}

Given any collection of extended lower reals, their \textbf{supremum} is an extended lower real which is found by taking the [[union]] of lower sets. The supremum of an inhabited set of lower reals is a lower real, and the supremum of an inhabited set of bounded lower reals is bounded iff the set has a bounded lower real as an upper bound. In any case, this supremum really is the [[supremum]] under $\leq$. This agrees with the notion of supremum of real numbers in the real number system, when that exists. Every extended lower real is also the supremum in this sense of its corresponding lower set, interpreted as a set of lower reals that happen to all be rational numbers.

Given any collection of extended upper reals, their \textbf{infimum} is an extended upper real which is found by taking the union of upper sets. The infimum of an inhabited set of upper reals is an upper real, and the infimum of an inhabited set of bounded upper reals is bounded iff the set has a bounded upper real as a lower bound. In any case, this infimum really is the [[infimum]] under $\leq$. This agrees with the notion of infimum of real numbers in the real number system, when that exists. Every extended upper real is also the infimum in this sense of its corresponding upper set, interpreted as a set of upper reals that happen to all be rational numbers.

By the [[adjoint functor theorem]], suprema of upper reals and infima of lower reals also exist, but they are not constructed as set-theoretic intersections but rather as the [[interior]] of an intersection. (This construction makes sense even in [[predicative mathematics|predicative]] constructive mathematics, though the adjoint functor theorem does not.) However, these may not be what we really want; an obvious example of this is if we take the infimum of a set of lower reals that happen to all be located, in which case what we really want is the corresponding \emph{upper} real infimum (for instance, when defining [[located subspaces]]). (In the [[MacNeille real numbers]], contained in both the lower and upper reals, both infima and suprema are constructed using interiors, and hence neither may be what we want.)

An [[inferior limit]] is \ldots{}

\hypertarget{arithmetic}{}\subsection*{{Arithmetic}}\label{arithmetic}

In general, you can extend [[order-preserving functions]] of rational numbers to lower reals and to upper reals; you simply take the [[image]] of the lower or upper set and close it downward or upwards, as appropriate. If you have an order-reversing function of rational numbers, then you can apply it to a lower real to get an upper real and conversely; this is about the only interaction that I know of between the two kinds of one-sided real.

Since addition is order-preserving, it works nicely, at least to make a [[monoid]]; but [[subtraction]] doesn't work in general. Multiplication has trouble with negative numbers but produces good results if you restrict to $[0,\infty]$. Notice that we get $0 \cdot \infty = 0$ with lower reals but $0 \cdot \infty = \infty$ with extended upper reals; thus, ${[{0,\infty}[}$ is a [[rig]] for either lower or upper reals, while $[0,\infty]$ is a rig only for lower reals. (This doesn't so much mean that upper reals behave worse than lower reals, as that extended reals on either side behave worse.) We can also use [[logarithms]] to translate between addition and multiplication. (In particular, $-\infty + \infty = -\infty$ with extended lower reals but $-\infty + \infty = \infty$ with extended upper reals.)

Of course, arithmetic with one-sided real numbers is much easier than this in [[classical mathematics]], where the bounded or extended versions may be identified; but even there, the natural operations involving $\pm\infty$ may differ. Accordingly, the conventions for arithmetic with infinities can signal which sort of number is appropriate for a [[constructive mathematics|constructive]] development.

If you want to do arbitrary arithmetic operations constructively on something more general than [[located real numbers]], you can try the [[MacNeille real number|MacNeille reals]], which are contained in both the upper and the lower reals.

\hypertarget{topology}{}\subsection*{{Topology}}\label{topology}

Let's put this on a separate page: [[semicontinuous topology]]. For one thing, it's more advanced than the elementary stuff above; for another thing, it's more interesting in classical mathematics; and finally, it's more complicated in constructive mathematics. The main point is that each type of one-sided real number has its own natural topology, and these differ (both classically and constructively) from the usual topology on the [[real line]].

\hypertarget{in_topos_theory}{}\subsection*{{In topos theory}}\label{in_topos_theory}

There is a bijective correspondence of [[internalization|internal]] extended lower real numbers in a sheaf topos $\mathrm{Sh}(X)$ of a [[topological space]] $X$ and [[semicontinuous map|lower semicontinuous]] functions $X \to \mathbb{R} \cup \{ +\infty \}$, or equivalently a [[continuous map|continuous]] function $X \to \mathbb{R} \cup \{ +\infty \}$, when the latter is equipped with the [[lower semicontinuous topology]]. (We will work classically in the external logic.)

Let $\Delta(\mathbb{Q})$ denote the [[constant sheaf]] of rational numbers on $X$. A \emph{lower real number} $U$ in $\mathrm{Sh}(X)$ is then defined as a subsheaf of $\Delta(\mathbb{Q})$ satisfying the axioms above (interpreted in the [[internal language]]). Such a lower real number induces a lower semicontinuous function $x \mapsto \sup U_x$, where $U_x$ denotes the [[stalk]] of $U$ at $x$ (taken as a subset of $\mathbb{Q}$).

Conversely, a lower semicontinuous function $f : X \to \mathbb{R} \cup \{ +\infty \}$ defines an internal lower real number $U$ with sections

\begin{displaymath}
U(A) \coloneqq \{ \varphi : A \to \mathbb{Q} | \forall x \in A: \varphi(x) \lt f(x) \} \subseteq \Delta(\mathbb{Q})(A)
\end{displaymath}
over open sets $A \subseteq X$.

See \hyperlink{Mulvey1974}{Mulvey (1974, page 28)} for details.

For the externally constructive version of this, it is best to take $X$ to be a [[locale]]; we need to use the (external) locale $L$ of lower real numbers in place of $\mathbb{R} \cup \{\infty\}$, and the notion of semicontinuous map is replaced with a continuous map (in the sense of locales) to $L$.

\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item D. Lesnik, \emph{Synthetic Topology and Constructive Metric Spaces} , PhD University of Ljubljana 2010. (\href{http://www.fmf.uni-lj.si/storage/19160/PhD_Davorin.pdf}{pdf})


\item [[Chris Mulvey|C. Mulvey]] (1974): \emph{Intuitionistic Algebra and Representations of Rings}. In Hofmann, Liukkonen: \emph{Recent Advances in the Representation Theory of Rings and C*-Algebras by Continuous Sections}, AMS 1974.


\item J. Z. Reichman, \emph{Semicontinuous Real Numbers in a Topos} , JPAA \textbf{28} (1983) pp.81-91.



\end{itemize}
See also the following MO-discussion: (\href{http://mathoverflow.net/questions/108029/simplification-in-semi-continuous-real?rq=1}{link})

[[!redirects one-sided real]] [[!redirects one-sided reals]] [[!redirects one-sided real number]] [[!redirects one-sided real numbers]] [[!redirects semicontinuous real]] [[!redirects semicontinuous reals]] [[!redirects semicontinuous real number]] [[!redirects semicontinuous real numbers]]

[[!redirects lower real]] [[!redirects lower reals]] [[!redirects lower real number]] [[!redirects lower real numbers]] [[!redirects bounded lower real]] [[!redirects bounded lower reals]] [[!redirects bounded lower real number]] [[!redirects bounded lower real numbers]] [[!redirects extended lower real]] [[!redirects extended lower reals]] [[!redirects extended lower real number]] [[!redirects extended lower real numbers]] [[!redirects lower semicontinuous real]] [[!redirects lower semicontinuous reals]] [[!redirects lower semicontinuous real number]] [[!redirects lower semicontinuous real numbers]]

[[!redirects upper real]] [[!redirects upper reals]] [[!redirects upper real number]] [[!redirects upper real numbers]] [[!redirects bounded upper real]] [[!redirects bounded upper reals]] [[!redirects bounded upper real number]] [[!redirects bounded upper real numbers]] [[!redirects extended upper real]] [[!redirects extended upper reals]] [[!redirects extended upper real number]] [[!redirects extended upper real numbers]] [[!redirects upper semicontinuous real]] [[!redirects upper semicontinuous reals]] [[!redirects upper semicontinuous real number]] [[!redirects upper semicontinuous real numbers]]



\end{document}