A Predicative Formula for Continuity at a Point, and the Set of Real-Valued Maps Continuous at a Point

In the setting of The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness, with predicative meant for formulas with abbreviations, conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards (ii) and guards as in Conditions Expressed by a Predicative Formula, and Guards (iii), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i). This helper is a statement of the metatheory. Let $(X,d)$ be a metric space and let $S\subseteq X$; $<$ is the strict order of the order $\le$ of $\mathbb{R}$.

(i) Let $(Y,e)$ be a metric space. The letters $g$ and $s$ are distinct set variables, and $S$, $d$, $Y$, $e$, $\mathbb{R}$, the strict order $<$ of $\mathbb{R}$ and its element $0$ are parameters. Let $\gamma(g,s)$ be the guard $\mu(g,S,Y)\wedge s\in S$, with $\mu$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii); it holds if and only if $g$ is a map $g:S\to Y$ and $s\in S$. Then the condition "$\gamma(g,s)$ holds and $g$ is continuous at $s$ relative to $S$", with $d$ and $e$ for the metrics $d_{X}$ and $d_{Y}$ of Continuous Map Between Metric Spaces (i), on $g$ and $s$, is expressed by a predicative formula.

(ii) Let $s_{0}\in S$, let $\mathbb{R}$ carry the distance $d_{\mathbb{R}}$, and let $\mathbb{R}^{S}$ be the set of maps from $S$ to $\mathbb{R}$. By (i), applied to the metric space $(\mathbb{R},d_{\mathbb{R}})$ of The Absolute Value Metric on the Real Numbers (i) in place of $(Y,e)$, there is a predicative formula $\psi(g,s)$ expressing that condition; and for every such $\psi$, with $s_{0}$ put for $s$, the class $\{g\in\mathbb{R}^{S}:\psi(g,s_{0})\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula (ii) is the same; it is written $C_{s_{0}}(S,d)$. It is a set and a subset of $\mathbb{R}^{S}$, and for every set $g$: $g\in C_{s_{0}}(S,d)$ if and only if $g$ is a map $g:S\to\mathbb{R}$ continuous at $s_{0}$ relative to $S$.