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

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

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

[[!include arithmetic geometry - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{history}{History}\dotfill \pageref*{history} \linebreak
\noindent\hyperlink{definitions_and_characterizations}{Definitions and characterizations}\dotfill \pageref*{definitions_and_characterizations} \linebreak
\noindent\hyperlink{Dedekind}{Dedekind cuts}\dotfill \pageref*{Dedekind} \linebreak
\noindent\hyperlink{cauchy_sequences}{Cauchy sequences}\dotfill \pageref*{cauchy_sequences} \linebreak
\noindent\hyperlink{the_complete_ordered_field}{The complete ordered field}\dotfill \pageref*{the_complete_ordered_field} \linebreak
\noindent\hyperlink{the_locale_of_real_numbers}{The locale of real numbers}\dotfill \pageref*{the_locale_of_real_numbers} \linebreak
\noindent\hyperlink{_as_a_terminal_coalgebra}{$\mathbb{R}$ as a terminal coalgebra}\dotfill \pageref*{_as_a_terminal_coalgebra} \linebreak
\noindent\hyperlink{Topologies}{Topologies}\dotfill \pageref*{Topologies} \linebreak
\noindent\hyperlink{generalisations}{Generalisations}\dotfill \pageref*{generalisations} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

A \emph{real number} is a [[number]] that may be [[Dedekind completion|approximated]] by [[rational numbers]]. Equipped with the operations of addition and multiplication induced from the rational numbers, real numbers form a \emph{[[field]]}, denoted $\mathbb{R}$. The underlying set is the \emph{[[Dedekind completion|completion]]} of the [[ordered field]] $\mathbb{Q}$ of rational numbers: the result of adjoining to $\mathbb{Q}$ [[suprema]] for every [[inhabited set|inhabited]] [[bounded set|bounded subset]] with respect to the natural [[order|ordering]] of rational numbers.

The [[set]] of real numbers also carries naturally the structure of a [[topological space]] and as such $\mathbb{R}$ is called the \emph{[[real line]]} also known as \emph{[[continuum|the continuum]]}. Equipped with both the topology and the field structure, $\mathbb{R}$ is a [[topological field]] and as such is the [[complete space|uniform completion]] of $\mathbb{Q}$ equipped with the [[absolute value]] [[metric space|metric]].

Together with its [[cartesian products]] -- the [[Cartesian spaces]] $\mathbb{R}^n$ for [[natural numbers]] $n \in \mathbb{N}$ -- the real line $\mathbb{R}$ is a standard formalization of the idea of \emph{continuous space}. The more general concept of ([[smooth manifold|smooth]]) \emph{[[manifold]]} is modeled on these Cartesian spaces. These, in turn are standard models for the notion of [[space]] in particular in [[physics]] (see \emph{[[spacetime]]}), or at least in [[classical physics]]. See at \emph{[[geometry of physics]]} for more on this.

\hypertarget{history}{}\subsection*{{History}}\label{history}

The original idea of a real number came from [[geometry]]; one thinks of a real number as specifying a \emph{point on a line}, with \emph{[[line]]} understood as the abstract idea of the object that a pencil and a ruler draw on a piece of paper. (More precisely, given two distinct points on the line, called $0$ and $1$, you get a [[bijection]] between the points and the real numbers.)

[[Euclid]] (citing [[Eudoxus]]) dealt with ratios of geometric magnitudes, which give positive real numbers; an arbitrary real number is then a difference of ratios of magnitudes. However, the Greeks did not think of such ratios as [[number]]s; that appears to have been an insight of the Arabs. See more at [[Eudoxus real number]].

A big project of the 19th century (at least in hindsight) was the `arithmetisation of analysis': showing how real numbers could be defined completely in terms of rational numbers (and the desired classes of functions on them could be defined in terms of the general point-set notion of [[function]]). Two successful approaches were developed in 1872, [[Richard Dedekind]]'s definition of real numbers as certain sets of rational numbers (called \emph{[[Dedekind cuts]]}) and [[Georg Cantor]]'s definition as certain sequences of rational numbers (called \emph{[[Cauchy sequences]]}).

A more modern approach is instead to characterise the properties that the set of real numbers must have and to prove that this is [[generalized the|categorical]] (unique up to a unique bijection preserving those properties). Then the important result of the 19th-century programme is simply that this is consistent (that there exists at least one such set). One can even use [[David Hilbert|Hilbert]]'s or [[Alfred Tarski|Tarski]]'s axioms for geometry to do this characterisation, coming full circle back to geometry.

Exactly how to define or characterise real numbers is still important in [[constructive mathematics]] and [[topos theory]] with its [[internal logic]]. For more on this, see [[real numbers object]] and the examples below.

\hypertarget{definitions_and_characterizations}{}\subsection*{{Definitions and characterizations}}\label{definitions_and_characterizations}

There are two basic approaches possible: to define what a \textbf{real number} is as a mathematical object, or to define the \textbf{real line} as a specific object in some previously known [[category]].

\hypertarget{Dedekind}{}\subsubsection*{{Dedekind cuts}}\label{Dedekind}

Consider two [[inhabited set|inhabited]] subsets, $L$ and $U$, of $\mathbb{Q}$ (the set of [[rational numbers]]) such that:

\begin{itemize}%
\item If $a \in L$, then $b \in L$ for some $b \gt a$.
\item If $b \in U$, then $a \in U$ for some $a \lt b$.
\item If $a \lt b$ are rational numbers, then $a \in L$ or $b \in U$. (*)
\item If $a \in L$ and $b \in U$, then $a \lt b$.

\end{itemize}
We may define a \textbf{Dedekind real number} to be such a pair, which is also called a \textbf{[[Dedekind cut]]}.

If $x \coloneqq (L,U)$ is a Dedekind cut, then we write $a \lt x$ to mean that $a \in L$ and $x \lt b$ to mean that $b \in U$.

We may approximate a Dedekind cut $x$ as closely as we like by applying (*) as often as necessary. This will be only finitely often, for any fixed positive level of approximation, given initial upper and lower bounds (which exist since $L$ and $U$ are inhabited).

See [[Dedekind cut]] for more.

\hypertarget{cauchy_sequences}{}\subsubsection*{{Cauchy sequences}}\label{cauchy_sequences}

Classically, a real number can be given by an [[infinite sequence]] of rational numbers, each of which is a decimal fraction that approximates the real number to a given number of decimal places. We can generalise this to any [[Cauchy sequence]] of rational numbers. However, now each real number has several representations, so we need to specify an [[equivalence relation]] on the Cauchy sequences. Thus, $\mathbb{R}$ is constructed as a [[subquotient]] of the [[function set]] $\mathbb{Q}^{\mathbb{N}}$.

This construction is equivalent to the construction by Dedekind cuts, at least assuming [[weak countable choice]] (which also follows from [[excluded middle]]). Thus it is popular in both [[classical mathematics]] and traditional [[constructive mathematics]] (which accepts [[countable choice]]). However, in stricter forms of constructive mathematics, including those used as [[internal languages]] in [[topos theory]], the Cauchy reals and Dedekind reals are not equivalent. (On the other hand, by generalising to Cauchy [[nets]], we recover the Dedekind reals again.)

See [[Cauchy real number]] for more.

\hypertarget{the_complete_ordered_field}{}\subsubsection*{{The complete ordered field}}\label{the_complete_ordered_field}

There is a well-known algebraic (more or less) characterisation of the real line as the `complete ordered field', or sometimes the `complete archimedean field'. This can be interpreted as follows:

\begin{itemize}%
\item A \textbf{field} is well known in algebra; if it matters, we mean a [[Heyting field]].
\item An \textbf{ordered field} means a \emph{[[linear order|linearly]]} ordered field.
\item An \textbf{archimedean field} is an ordered field in which every element is bounded above by a [[natural number]], so it has no [[infinite number|infinite]] elements (and thus no non-zero [[infinitesimal number|infinitesimal]] elements).
\item An ordered field is \textbf{complete} if it is [[Dedekind completion|Dedekind-complete]].
\item Alternatively, an archimedean field is \textbf{complete} if it is [[terminal object|terminal]] in the category of archimedean fields.

\end{itemize}
We speak of [[the]] such field because it is unique up to unique [[isomorphism]].

\begin{utheorem}
There is an archimedean field $\mathbb{R}$ which is both Dedekind-complete and terminal among archimedean fields. Furthermore, every Dedekind-complete ordered field is isomorphic to $\mathbb{R}$. (By [[abstract nonsense]], we already know that every terminal archimedean field is isomorphic to $\mathbb{R}$ and that $\mathbb{R}$ has only the identity [[automorphism]], so isomorphisms to it are unique.)

\end{utheorem}
\begin{proof}
Construct $\mathbb{R}$ using, say, Dedekind cuts of rational numbers. Then it is well known how to prove these facts about $\mathbb{R}$, so we omit the proof for now.

\end{proof}
However, we note that the proof is valid in weak [[foundations]], in particular internal to any [[topos]] with a [[natural numbers object]]. One can actually work in even weaker foundations than that; see the constructions at [[real numbers object]]. Even weaker foundations are possible if one allows the [[underlying set]] of $\mathbb{R}$ to be [[proper class|large]].

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

Consider a [[binary relation]] $\sim$ on [[rational numbers]] satisfying these four properties:

\begin{itemize}%
\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{itemize}
These relations form a [[frame]], which we may interpret (by definition) as the \textbf{[[locale of real numbers]]}. It can also be defined as the [[localic completion]] of the rational numbers.

We may then define a \textbf{localic real number} to be a [[point of a locale|point]] of this locale.

This agrees with the notion of Dedekind real number, even in very weak ([[predicative mathematics|predicative]] and [[constructive mathematics|constructive]]) [[foundations]].

See [[locale of real numbers]] for more.

\hypertarget{_as_a_terminal_coalgebra}{}\subsubsection*{{$\mathbb{R}$ as a terminal coalgebra}}\label{_as_a_terminal_coalgebra}

The real line $\mathbb{R}$, or at least the positive real line $\mathbb{R}^+$, may be characterized as the [[terminal object|terminal]] [[coalgebra for an endofunctor]]

Let [[Pos]] be the [[category]] of [[poset]]s. Consider the endofunctor

\begin{displaymath}
F_1\colon Pos \to Pos
\end{displaymath}
that acts by [[ordinal product]] with $\omega$

\begin{displaymath}
F_1\colon X \mapsto X \cdot \omega
  \,.
\end{displaymath}
\begin{uprop}
The terminal coalgebra of $F_1$ is order isomorphic to the non-negative real line $\mathbb{R}^+$, with its standard order.

\end{uprop}
\begin{proof}
This is theorem 5.1 in

\begin{itemize}%
\item D. Pavlovic, [[Vaughan Pratt]], \emph{On coalgebra of real numbers} (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.5204}{web})

\end{itemize}
\end{proof}
There are more and similar characterizations along these lines. One is an example at [[final coalgebra]].

\hypertarget{Topologies}{}\subsection*{{Topologies}}\label{Topologies}

There are alternative topologies on $\mathbb{R}$ sometimes considered:

\begin{itemize}%
\item the [[discrete topology]] (not very interesting),
\item the [[order topology]] or [[absolute-value topology]] (the usual topology of a [[Euclidean space|Euclidean]] [[metric space]]),
\item the [[upper-interval topology]] or the [[lower-interval topology]],
\item the [[lower semicontinuous topology]] or the [[upper semicontinuous topology]],
\item the [[K-topology]].

\end{itemize}
Another variant of $\mathbb{R}$ as a topological space is the

\begin{itemize}%
\item [[long line]].

\end{itemize}
\hypertarget{generalisations}{}\subsection*{{Generalisations}}\label{generalisations}

The term `real number' was originally introduced to indicate that one is \emph{not} considering the generalistion to [[complex numbers]] or other kinds of [[hypercomplex numbers]]. Accordingly, that term `real' may sometimes be used for another generalisation of real numbers to indicate again that one is not considering a complexification.

The [[extended real number]]s include $\pm\infty$ as well as the real numbers; one may speak of \emph{finite numbers} or \emph{bounded numbers} to indicate that one is not considering this extension. [[lower real|Lower reals]], [[upper reals]], and [[MacNeille real number|MacNeille reals]] are related generalisations studied in [[constructive mathematics]], although with [[excluded middle]] they are (at least if bounded) the same as ordinary real numbers; one may speak of \emph{located numbers} to indicate that one is not considering such extensions.

[[surreal number|Surreal numbers]] and the [[hyperreal number]]s of [[nonstandard analysis]] are two ways to include [[infinite number|infinite]] and [[infinitesimal number|infinitesimal]] versions of real numbers (besides the trivial case of $\pm\infty$); one may speak of \emph{standard numbers} to indicate that one is not considering such extensions (although the precise meaning of `standard' depends on the [[universe]] that one is working in).

In [[descriptive set theory]], one often says `real number' for an element of [[Baire space of irrational numbers|Baire space]] $\mathbb{N}^{\mathbb{N}}$. This is not really a generalisation; by the [[Schroeder-Bernstein theorem]], the sets $\mathbb{R}$ and $\mathbb{N}^{\mathbb{N}}$ are [[bijection|isomorphic]]. Constructively, $\mathbb{N}^{\mathbb{N}}$ can still be thought of as the set of [[irrational numbers]], so this use of the term may actually be a \emph{restriction}.

[[floating-point number|Floating-point numbers]] are often used in computer programming to represent real numbers, but they do not behave very well; one may speak of \emph{infinite-precision numbers} to indicate that one's programming environment models `\href{http://math.fau.edu/richman/html/mm2.htm}{\emph{real} real numbers}'.

As mentioned above, the $p$-[[adic number|adic numbers]] for various [[prime numbers]] $p$ are variations on the theme of real numbers; real numbers may be thought of as \emph{$0$-adic numbers}. Similarly, the real numbers are \emph{characteristic-$0$ numbers} since they are based on the [[prime field]] $\mathbb{Q}$; one could also start the construction with a different [[characteristic]] (although it makes more sense to get analogues of complex numbers than of real numbers).

Finally, one can consider points on a [[noncommutative geometry|noncommutative]] line instead of the usual \emph{commutative numbers}.

So in summary, this page is about the \emph{real, finite, located, standard, analytic, infinite-precision, $0$-adic, characteristic-$0$, commutative numbers}.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[real numbers object]]


\item [[computable real number]]


\item [[p-adic numbers]]


\item in [[constructive analysis]] one may use the [[completion monad]] for dealing with real numbers


\item [[exact real computer arithmetic]]



\end{itemize}
[[!include exceptional spinors and division algebras -- table]]

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

A formalization of the real numbers in [[homotopy type theory]] is in

\begin{itemize}%
\item [[Univalent Foundations Project]], chapter 11 of \emph{[[Homotopy Type Theory – Univalent Foundations of Mathematics]]}


\item Ga\"e{}tan Gilbert, \emph{Formalising Real Numbers in Homotopy Type Theory} (\href{https://arxiv.org/abs/1610.05072}{arXiv:1610.05072})



\end{itemize}
For more see the references at \emph{[[analysis]]}.

[[!redirects real number]] [[!redirects real numbers]]

[[!redirects real line]] [[!redirects real number line]] [[!redirects the continuum]]

[[!redirects located real number]] [[!redirects located real numbers]] [[!redirects located Dedekind real number]] [[!redirects located Dedekind real numbers]]



\end{document}