Kit for def:continuous-map-metric-spaces

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity, let $n\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{n-1}$ be distinct set variables, and let $i,j,k,l,m,p,q<n$, not necessarily distinct. A condition on $x_{0},\dots,x_{n-1}$ is predicative if it is expressed by a predicative formula, with $x_{0},\dots,x_{n-1}$ in place of the set variables listed in Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables; $\mathbb{R}$, the addition $+$, the element $0$ and the order $\le$ of $\mathbb{R}$ are parameters. Metric spaces are as in Metric Space (vi), subsets as in Subclasses and Subsets (i), maps, and continuity at a point and on a subset as in Continuous Map Between Metric Spaces (i) and Continuous Map Between Metric Spaces (ii). In the first four clauses $X=x_{i}$, $d_{X}=x_{j}$, $Y=x_{k}$, $d_{Y}=x_{l}$, $A=x_{m}$, $f=x_{p}$ and $x=x_{q}$, where these letters occur.

(i) Continuity at a point. The condition "$(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces, $A\subseteq X$, $f$ is a map $f:A\to Y$, $x\in A$, and $f$ is continuous at $x$ relative to $A$" on $x_{0},\dots,x_{n-1}$ is predicative.

(ii) Continuity at a point of the space. The condition "$(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces, $f$ is a map $f:X\to Y$, $x\in X$, and $f$ is continuous at $x$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iii) Continuity on a subset. The condition "$(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces, $A\subseteq X$, $f$ is a map $f:A\to Y$, and $f$ is continuous on $A$" on $x_{0},\dots,x_{n-1}$ is predicative.

(iv) Continuous maps. The condition "$(X,d_{X})$ and $(Y,d_{Y})$ are metric spaces, $f$ is a map $f:X\to Y$, and $f$ is continuous" on $x_{0},\dots,x_{n-1}$ is predicative.

(v) The class of maps continuous at a point. For all metric spaces $(X,d_{X})$ and $(Y,d_{Y})$, every $A\subseteq X$ and every $x\in A$ there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a map $f:A\to Y$ that is continuous at $x$ relative to $A$.

(vi) The class of maps of the space continuous at a point. For all metric spaces $(X,d_{X})$ and $(Y,d_{Y})$ and every $x\in X$ there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a map $f:X\to Y$ that is continuous at $x$.

(vii) The class of maps continuous on a subset. For all metric spaces $(X,d_{X})$ and $(Y,d_{Y})$ and every $A\subseteq X$ there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a map $f:A\to Y$ that is continuous on $A$.

(viii) The class of continuous maps. For all metric spaces $(X,d_{X})$ and $(Y,d_{Y})$ there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a continuous map $f:X\to Y$.