Kit for def:derivative-real-interval

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and The Real Line: Standing Notation and Background for Calculus on Intervals; this item is a statement of the metatheory. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j,k,l<N$, not necessarily distinct. Each of the first six clauses states that a condition on $x_{0},\dots,x_{N-1}$ is predicative: expressed by a predicative formula, with $x_{0},\dots,x_{N-1}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i) and no displayed variables. The other letters, $\mathbb{R}$, its operations $+$ and $\cdot$, its elements $0$ and $1$, its order $\le$ and the strict order $<$ of $\le$, are parameters. Class comprehension (The Class Comprehension Theorem for Predicative Formulas (i)) and induction (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)) apply to such formulas, among them the readings of formula trees (The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii)). Subsets are as in Subclasses and Subsets (i) and maps as in Functions, Values of a Function, and Functions from One Class to Another (iii). In the first six clauses the letters stand for arbitrary sets, so each condition there includes the standing hypotheses of Derivative of a Real Function on an Interval; in the last three, $I$, and $x$ or $S$ where they occur, are fixed, so that the condition is on $f$ alone. The $\varepsilon$-$\delta$ condition of Derivative of a Real Function on an Interval (i) taken apart from these hypotheses is not a notion of the definition and has no clause; under them it coincides with the condition of (ii). There is no class clause for the hypotheses, for derivatives at a point or for the derivative map: with $I$ and $f$ fixed, the class of the $u$ satisfying the hypotheses is $I$ or empty, and with $I$ and $f$ (and $x$) fixed the classes of derivatives $L$ of $f$ at $x$ and of maps $g=f'$ have at most one element, by Uniqueness of the Derivative of a Real Function on an Interval (i).

(i) The standing hypotheses. With $I=x_{i}$, $f=x_{j}$ and $u=x_{k}$, the condition "$I$ is an interval containing two distinct points, $f$ is a map $f:I\to\mathbb{R}$, and $u\in I$" is predicative.

(ii) Derivatives at a point. With $I=x_{i}$, $f=x_{j}$, $x=x_{k}$ and $L=x_{l}$, the condition "$I$ is an interval containing two distinct points, $f$ is a map $f:I\to\mathbb{R}$, $x\in I$, $L\in\mathbb{R}$, and $L$ is a derivative of $f$ at $x$" is predicative.

(iii) Differentiability at a point. With $I=x_{i}$, $f=x_{j}$ and $x=x_{k}$, the condition "$I$ is an interval containing two distinct points, $f$ is a map $f:I\to\mathbb{R}$, $x\in I$, and $f$ is differentiable at $x$" is predicative.

(iv) Differentiability on a subset. With $I=x_{i}$, $f=x_{j}$ and $S=x_{k}$, the condition "$I$ is an interval containing two distinct points, $f$ is a map $f:I\to\mathbb{R}$, $S\subseteq I$, and $f$ is differentiable on $S$" is predicative.

(v) Differentiable maps. With $I=x_{i}$ and $f=x_{j}$, the condition "$I$ is an interval containing two distinct points and $f$ is a differentiable map $f:I\to\mathbb{R}$" is predicative.

(vi) The derivative map. With $I=x_{i}$, $f=x_{j}$ and $g=x_{k}$, the condition "$I$ is an interval containing two distinct points, $f$ is a differentiable map $f:I\to\mathbb{R}$, and $g$ is the derivative $f'$ of $f$" is predicative.

(vii) The class of maps differentiable at a point. For every interval $I$ containing two distinct points and every $x\in I$ there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a map $f:I\to\mathbb{R}$ that is differentiable at $x$.

(viii) The class of maps differentiable on a subset. For every interval $I$ containing two distinct points and every $S\subseteq I$ there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a map $f:I\to\mathbb{R}$ that is differentiable on $S$.

(ix) The class of differentiable maps. For every interval $I$ containing two distinct points there is a class $C$ such that, for every class $f$, $f\in C$ if and only if $f$ is a differentiable map $f:I\to\mathbb{R}$.