Kit for def:lebesgue-integral-integrable

In the setting of Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity and Measurable Functions and the Lebesgue Integral: Notation, let $(X,\mathcal{F})$ be a measurable space. Let $N\ge1$ be a metatheoretic number, let $x_{0},\dots,x_{N-1}$ be distinct set variables, and let $i,j<N$, not necessarily distinct. The parameters, each other than $x_{0},\dots,x_{N-1}$, are the set variables $X$ and $\mathcal{F}$; the ten parameters of Kit for def:measure-measure-space; and the parameters of The Simple, Nonnegative, Integrable and Signed Integrals Are Predicative in the Measure and the Function, at Any Variable Positions (iii) for $(X,\mathcal{F})$; the last two groups with the kinds and values given there. In the first two clauses, 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 variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these parameters.

(i) Integrable functions. With $\mu=x_{i}$ and $f=x_{j}$, the condition "$\mu$ is a measure on $(X,\mathcal{F})$ and $f$ lies in the set $\mathcal{L}^{1}(\mu)$" is predicative.

(ii) The integral as a map. With $\mu=x_{i}$ and $I=x_{j}$, the condition "$\mu$ is a measure on $(X,\mathcal{F})$ and $I$ is the integral with respect to $\mu$, the map $\mathcal{L}^{1}(\mu)\to\mathbb{R}$, $f\mapsto\int f\,d\mu$" is predicative.

(iii) The class of integrable functions. For every measure $\mu$ on $(X,\mathcal{F})$ there is a class $C$ such that, for every class $a$, $a\in C$ if and only if $a\in\mathcal{L}^{1}(\mu)$; and $C$ is the set $\mathcal{L}^{1}(\mu)$.

(iv) The class of integral maps. For every measure $\mu$ on $(X,\mathcal{F})$ there is a class $D$ such that, for every class $a$, $a\in D$ if and only if $a$ is the integral with respect to $\mu$; and $D$ is a set, namely the singleton whose only element is the integral with respect to $\mu$.