Kit for def:measurable-function

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<N$, not necessarily distinct. Let $\mathbb{N}$, $R$, $\mathbb{R}$, $\mathcal{B}(\mathbb{R})$, $[0,\infty]$ and $\mathcal{B}([0,\infty])$ be distinct class variables with values, in this order, the set $\mathbb{N}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii), the order $\le$ of $\mathbb{N}_{0}$, the set of real numbers, the Borel $\sigma$-algebra of Borel Sigma-Algebra of a Metric Space (ii), the set $[0,\infty]$ of The Extended Real Line, Its Order, and [0,∞] (ii) and the Borel $\sigma$-algebra of The Borel σ-Algebra of [0,∞] (ii); each is denoted below by the symbol for its value. 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}$ as the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these six class variables as parameters.

(i) Measurable maps. With $X=x_{i}$, $\mathcal{F}=x_{j}$, $Y=x_{k}$, $\mathcal{G}=x_{l}$ and $f=x_{m}$, the condition "$(X,\mathcal{F})$ and $(Y,\mathcal{G})$ are measurable spaces and $f$ is a map $f:X\to Y$ that is $\mathcal{F}/\mathcal{G}$-measurable" is predicative.

(ii) Maps into $\mathbb{R}$. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $f=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space and $f$ is a map $f:X\to\mathbb{R}$ that is measurable as a map into $\mathbb{R}$" is predicative.

(iii) Maps into $\mathbb{R}^{n}$. With $X=x_{i}$, $\mathcal{F}=x_{j}$, $n=x_{k}$ and $f=x_{l}$, the condition "$(X,\mathcal{F})$ is a measurable space, $n\in\mathbb{N}$, and $f$ is a map $f:X\to\mathbb{R}^{n}$ into Euclidean space that is measurable as a map into $\mathbb{R}^{n}$" is predicative.

(iv) Maps into $\mathbb{R}^{p\times q}$. With $X=x_{i}$, $\mathcal{F}=x_{j}$, $p=x_{k}$, $q=x_{l}$ and $f=x_{m}$, the condition "$(X,\mathcal{F})$ is a measurable space, $p,q\in\mathbb{N}$, and $f$ is a map $f:X\to\mathbb{R}^{p\times q}$ into the set of real $p\times q$ matrices that is measurable as a map into $\mathbb{R}^{p\times q}$" is predicative.

(v) Maps into $[0,\infty]$. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $f=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space and $f$ is a map $f:X\to[0,\infty]$ that is measurable as a map into $[0,\infty]$" is predicative.