\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*{located subspace}

\hypertarget{located_subspaces}{}\section*{{Located subspaces}}\label{located_subspaces}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{in_metric_spaces}{In metric spaces}\dotfill \pageref*{in_metric_spaces} \linebreak
\noindent\hyperlink{in_uniform_spaces}{In uniform spaces}\dotfill \pageref*{in_uniform_spaces} \linebreak
\noindent\hyperlink{in_topological_spaces}{In topological spaces}\dotfill \pageref*{in_topological_spaces} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{singletons}{Singletons}\dotfill \pageref*{singletons} \linebreak
\noindent\hyperlink{covert_subsets}{Covert subsets}\dotfill \pageref*{covert_subsets} \linebreak
\noindent\hyperlink{compact_subspaces}{Compact subspaces}\dotfill \pageref*{compact_subspaces} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

In [[constructive mathematics|constructive]] point-set [[topology]], there are a variety of notions of when a [[subspace]] is \emph{located}. This varies depending on what kind of space one is discussing, and even for a given kind of space, there are sometimes various weaker and stronger notions of locatedness. Typically (if not always), these concepts are trivial in [[classical mathematics]].

A located subspace should be viewed as a \emph{nice} subspace, ruling out pathological counterexamples that exist for logical rather than topological reasons. For example, given any space $X$ and any [[truth value]] $p$, there exists a subspace $\{x | p\}$, and these can seem very strange for undecidable $p$; but typically (if not always), this subspace will only be located if $p$ is true or false.

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

\hypertarget{in_metric_spaces}{}\subsubsection*{{In metric spaces}}\label{in_metric_spaces}

Given a [[metric space]] $X$, a [[subspace]] $S$ of $X$, and a [[point]] $x$ of $X$, we commonly define the \textbf{distance} from $x$ to $S$ (or from $S$ to $x$) as an [[infimum]]:

\begin{displaymath}
d(x,S) \coloneqq \inf_{y \in S} d(x,y) .
\end{displaymath}
In [[constructive mathematics]], this infimum is generally an [[upper real number]], even if (as is usual) we require the distances $d(x,y)$ to always be a [[located real number]].

The subspace $S$ is \textbf{located} (or \textbf{metrically located} to be specific) if, for each point $x$, $d(x,S)$ is located. (Although we are defining located subspaces in terms of located real numbers, this is backwards historically; the term was first used, by [[Jan Brouwer]], to refer to subsets.)

We should really speak of [[extended real number|extended]] upper/located real numbers, in case $S$ might be empty or we wish to apply the concept in an [[extended metric space]]. But at least if $X$ is [[bounded metric space|bounded]] and [[inhabited space|inhabited]], then a located subspace $S$ must be empty or inhabited.

Note that there is a smaller complete lattice than the upper reals that contains the located reals and in which we could take the infimum, namely the [[MacNeille real numbers]]. However, the inclusion of MacNeille reals into upper reals does not preserve infima (though it does preserve suprema), and in the definition of located subspace we really do want to assert that the \emph{upper real} infimum, not the MacNeille real infimum, is a located real. This is because upper real infima, unlike MacNeille real infima, have the property that if $\inf A \lt \varepsilon$ then there is an $a\in A$ such that $a\lt\varepsilon$, which is crucial for the desired behavior of locatedness.

\hypertarget{in_uniform_spaces}{}\subsubsection*{{In uniform spaces}}\label{in_uniform_spaces}

If $X$ is a [[uniform space]], \hyperlink{BridgesAL}{Bridges et. al.} define a subspace $S$ to be \textbf{almost located} if for any entourage $U$, there is an entourage $V$ such that $\neg V[S] \cup U[S] = X$. In other words, every point $x\in X$ is either within $U$ of some point of $S$ or not within $V$ of any point of $S$.

Since this seems the most natural notion of locatedness for uniform spaces, one might naturally also call such a subspace \textbf{uniformly located}. However, note that even if $X$ is a metric space, metric locatedness is strictly stronger than uniform locatedness; Bridges et. al. give an example showing that metric locatedness is not a uniform invariant (while uniform locatedness is of course).

\hypertarget{in_topological_spaces}{}\subsubsection*{{In topological spaces}}\label{in_topological_spaces}

Given a [[topological space]] $X$ and a [[subspace]] $S$ of $X$, $S$ is \textbf{located} (or \textbf{topologically located} to be specific) if, given any point $x$ and neighbourhood $U$ of $x$, either $U \cap S$ is [[inhabited subset|inhabited]] or some other neighbourhood $V$ of $x$ is [[disjoint subsets|disjoint]] with $S$.

See Section 7.3 of \hyperlink{TvD}{Troelstra \& van Dalen}.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{singletons}{}\subsubsection*{{Singletons}}\label{singletons}

Any singleton subset of a metric space, or more generally any finite subset, is metrically located, since we can take the minimum of any finite set. A singleton subset of a uniform space is uniformly located if and only if the uniform space is [[regular space|regular]].

\hypertarget{covert_subsets}{}\subsubsection*{{Covert subsets}}\label{covert_subsets}

\begin{utheorem}
Suppose $X$ is a [[uniformly regular space|uniformly regular]] uniform space and that (the underlying set of) $S\subseteq X$ is a [[covert set]]. Then $S$ is uniformly located in $X$.

\end{utheorem}
\begin{proof}
Since $X$ is uniformly regular, for any entourage $U$ there is an entourage $V$ such that $\neg V \cup U = X\times X$. In particular, for any $x\in X$, for any $y\in S$, we have either $(x,y)\in U$ or $(x,y)\notin V$. By covertness of $S$, it follows that either $(x,y)\in U$ for some $y\in S$, or $(x,y)\notin V$ for all $y\in S$, which is to say that $x\in \neg V[S] \cup U[S]$.

\end{proof}
\hypertarget{compact_subspaces}{}\subsubsection*{{Compact subspaces}}\label{compact_subspaces}

\begin{utheorem}
Suppose $X$ is a [[uniformly regular space|uniformly regular]] uniform space and that $S\subseteq X$ is [[compact space|compact]] in its induced topology. Then $S$ is uniformly located in $X$.

\end{utheorem}
\begin{proof}
Given any entourage $U$, let $V$ and $W$ be entourages such that $\neg V \cup U = X\times X$ (by uniform regularity) and $W\circ W\circ W \subseteq V$. Let $G$ be the interior of $\neg W$. Then $\neg V \subseteq G$, since if $(x,y)\notin V$ then $W[x] \times W[y]$ is a neighborhood of $(x,y)$ contained in $\neg W$ (for if $x \approx_W w \approx_W z \approx_W y$ then $(x,y)\in V$, which is not the case, hence $(w,z)\notin W$). Thus, $G\cup U = X\times X$.

Let $i: X\times S \to X\times X$ be the inclusion and $\pi : X\times S \to X$ the projection. Then $i^* G \cup i^* U = X\times S$. Since $X$ is uniformly regular, it is regular. Thus $S$ is compact regular, and hence locally compact, so the locale product $X\times S$ is spatial. Therefore $\pi$ is both an [[open map]] and a [[proper map]] of [[locales]]. We then have $i^* G \cup \pi^* \pi_! i^* U = X\times S$, hence $\pi_*(i^* G \cup \pi^* \pi_! i^* U) = X$, and so by properness $\pi_* i^* G \cup \pi_! i^* U = X$ as well. In other words, for every $x\in X$ either $(x,y)\in G$ for all $y\in S$, or there exists a $y\in S$ such that $(x,y)\in U$. Since $G\subseteq \neg W$, it follows that $S$ is almost located.

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

\begin{itemize}%
\item [[Douglas Bridges]], Hajime Ishihara, Ray Mines, [[Fred Richman]], Peter Schuster, and Luminia V\^i{}. \emph{Almost locatedness in uniform spaces}, Czechoslovak Mathematical Journal, Vol. 57 (2007), No. 1, 1--12, \href{http://dml.cz/dmlcz/128150}{web}


\item [[Anne Sjerp Troelstra]] \& [[Dirk van Dalen]], \emph{Constructivism in Mathematics} 2.



\end{itemize}
Various related notions of locatedness are studied in

\begin{itemize}%
\item [[Frank Waaldijk]], \emph{modern intuitionistic topology}, Ph.D. Thesis, \href{http://www.fwaaldijk.nl/modern%20intuitionistic%20topology.pdf}{link}

\end{itemize}
[[!redirects located set]] [[!redirects located sets]] [[!redirects located subset]] [[!redirects located subsets]] [[!redirects located subspace]] [[!redirects located subspaces]]

[[!redirects metrically located set]] [[!redirects metrically located sets]] [[!redirects metrically located subset]] [[!redirects metrically located subsets]] [[!redirects metrically located subspace]] [[!redirects metrically located subspaces]]

[[!redirects uniformly located set]] [[!redirects uniformly located sets]] [[!redirects uniformly located subset]] [[!redirects uniformly located subsets]] [[!redirects uniformly located subspace]] [[!redirects uniformly located subspaces]]

[[!redirects topologically located set]] [[!redirects topologically located sets]] [[!redirects topologically located subset]] [[!redirects topologically located subsets]] [[!redirects topologically located subspace]] [[!redirects topologically located subspaces]]

[[!redirects almost located set]] [[!redirects almost located sets]] [[!redirects almost located subset]] [[!redirects almost located subsets]] [[!redirects almost located subspace]] [[!redirects almost located subspaces]]



\end{document}