Predicative Formulas for Upper and Lower Darboux Sums, and the Maps and Sets of Darboux Sums over All Partitions

In the setting of The Real Line: Standing Notation and Background for Calculus on Intervals, 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), with parameters and their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); (i) is a statement of the metatheory. For $a,b\in\mathbb{R}$ with $a<b$, partitions of $[a,b]$ and the set of partitions $\Pi_{a,b}$ are as in Partitions of a Closed Interval, the Set of Partitions, and Refinements (i) and Partitions of a Closed Interval, the Set of Partitions, and Refinements (ii); a map $f:[a,b]\to\mathbb{R}$ is bounded if there is $B\in\mathbb{R}$ with $|f(t)|\le B$ for every $t\in[a,b]$; and for such a bounded $f$ and a partition $P$ of $[a,b]$, $U(f,P)$ and $L(f,P)$ are the upper sum and the lower sum of Upper and Lower Darboux Sums of a Bounded Function on a Partition (ii) and Upper and Lower Darboux Sums of a Bounded Function on a Partition (iii).

(i) The letters $a$, $b$, $f$, $P$ and $z$ are distinct set variables, and $\mathbb{R}$, its operations $+$ and $\cdot$, its elements $0$ and $1$, its order $\le$ and the strict order $<$ of $\le$, and $\mathbb{N}$, $\mathbb{N}_{0}$ and the order $\le$, the addition $+$ and the element $1$ of $\mathbb{N}_{0}$ are parameters. Then the condition "$a,b\in\mathbb{R}$, $a<b$, $f$ is a bounded map $f:[a,b]\to\mathbb{R}$, $P\in\Pi_{a,b}$ and $z=U(f,P)$" on $a$, $b$, $f$, $P$ and $z$ is expressed by a predicative formula, and so is the condition obtained from it by putting $L(f,P)$ for $U(f,P)$. In particular, for fixed $a,b\in\mathbb{R}$ with $a<b$, taken as further parameters, the condition "$f$ is a bounded map $f:[a,b]\to\mathbb{R}$, $P\in\Pi_{a,b}$ and $z=U(f,P)$" on $f$, $P$ and $z$, and the same condition with $L(f,P)$ for $U(f,P)$, are expressed by predicative formulas.

(ii) Let $a,b\in\mathbb{R}$ with $a<b$, and let $f:[a,b]\to\mathbb{R}$ be bounded. There is exactly one map from $\Pi_{a,b}$ to $\mathbb{R}$ with value $U(f,R)$ at every $R\in\Pi_{a,b}$, the map $R\mapsto U(f,R)$, and exactly one with value $L(f,R)$ at every $R\in\Pi_{a,b}$, the map $R\mapsto L(f,R)$. The classes $\{U(f,R):R\in\Pi_{a,b}\}$ and $\{L(f,R):R\in\Pi_{a,b}\}$, formed by class abstraction with formulas provided by (i), are sets and subsets of $\mathbb{R}$; and for every set $s$: $s\in\{U(f,R):R\in\Pi_{a,b}\}$ if and only if $s=U(f,R)$ for some $R\in\Pi_{a,b}$, and $s\in\{L(f,R):R\in\Pi_{a,b}\}$ if and only if $s=L(f,R)$ for some $R\in\Pi_{a,b}$.