Kit for def:measure-measure-space

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<n$, not necessarily distinct. Let $E$, $L$, $Z$, $P$, $\mathbb{N}$, $R$ and $Q$ be distinct class variables with the values of the class variables $E$, $L$, $Z$, $P$, $N$, $R$ and $Q$ of Sums of Sequences in [0,∞] as Typed Terms and as a Map (i) (its $N$ being written $\mathbb{N}$ here), and let $\infty$, $0$ and $1$ be distinct set variables, other than $x_{0},\dots,x_{n-1}$, whose values are the element $\infty$ of The Extended Real Line, Its Order, and [0,∞] (i) and the real numbers $0$ and $1$, which lie in $[0,\infty]$ (Addition and Multiplication on [0,∞] (ii)). In the first six 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}$ as the variables of Conditions Expressed by a Predicative Formula, and Guards (i), no displayed variables, and these ten variables as parameters.

(i) Pairwise disjoint sequences. With $\mathcal{F}=x_{i}$ and $a=x_{j}$, the condition "$a$ is a sequence in $\mathcal{F}$ and $a(m)\cap a(l)=\emptyset$ for all $m,l\in\mathbb{N}$ with $m\neq l$" is predicative, where $a(m)$ is the value of $a$ at $m$, $\cap$ the intersection and $\emptyset$ the empty set.

(ii) Measures. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $\mu=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space and $\mu$ is a measure on $(X,\mathcal{F})$" is predicative.

(iii) Measure spaces. With $M=x_{i}$, the condition "$M$ is a measure space" is predicative.

(iv) Finite measures. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $\mu=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space, $\mu$ is a measure on $(X,\mathcal{F})$, and $\mu$ is finite" is predicative.

(v) $\sigma$-finite measures. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $\mu=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space, $\mu$ is a measure on $(X,\mathcal{F})$, and $\mu$ is $\sigma$-finite" is predicative.

(vi) Probability measures. With $X=x_{i}$, $\mathcal{F}=x_{j}$ and $\mu=x_{k}$, the condition "$(X,\mathcal{F})$ is a measurable space and $\mu$ is a probability measure on $(X,\mathcal{F})$" is predicative.

(vii) The set of pairwise disjoint sequences. For every set $\mathcal{F}$ there is a class $\mathcal{D}$ such that, for every class $a$, $a\in\mathcal{D}$ if and only if $a$ is a sequence in $\mathcal{F}$ and $a(m)\cap a(l)=\emptyset$ for all $m,l\in\mathbb{N}$ with $m\neq l$; and $\mathcal{D}$ is a set and a subset of the set $\mathcal{F}^{\mathbb{N}}$ of functions from $\mathbb{N}$ to $\mathcal{F}$.

(viii) The set of measures on a measurable space. For all sets $X$ and $\mathcal{F}$ such that $(X,\mathcal{F})$ is a measurable space, there is a class $\mathcal{M}$ such that, for every class $\mu$, $\mu\in\mathcal{M}$ if and only if $\mu$ is a measure on $(X,\mathcal{F})$; and $\mathcal{M}$ is a set and a subset of the set $[0,\infty]^{\mathcal{F}}$ of functions from $\mathcal{F}$ to $[0,\infty]$.

(ix) The class of measure spaces. There is a class $\mathcal{S}$ such that, for every class $M$, $M\in\mathcal{S}$ if and only if $M$ is a measure space.

(x) The set of finite measures. For all sets $X$ and $\mathcal{F}$ such that $(X,\mathcal{F})$ is a measurable space, there is a class $\mathcal{M}_{\mathrm{fin}}$ such that, for every class $\mu$, $\mu\in\mathcal{M}_{\mathrm{fin}}$ if and only if $\mu$ is a measure on $(X,\mathcal{F})$ and $\mu$ is finite; and $\mathcal{M}_{\mathrm{fin}}$ is a set and a subset of $[0,\infty]^{\mathcal{F}}$.

(xi) The set of $\sigma$-finite measures. For all sets $X$ and $\mathcal{F}$ such that $(X,\mathcal{F})$ is a measurable space, there is a class $\mathcal{M}_{\sigma}$ such that, for every class $\mu$, $\mu\in\mathcal{M}_{\sigma}$ if and only if $\mu$ is a measure on $(X,\mathcal{F})$ and $\mu$ is $\sigma$-finite; and $\mathcal{M}_{\sigma}$ is a set and a subset of $[0,\infty]^{\mathcal{F}}$.

(xii) The set of probability measures. For all sets $X$ and $\mathcal{F}$ such that $(X,\mathcal{F})$ is a measurable space, there is a class $\mathcal{M}_{1}$ such that, for every class $\mu$, $\mu\in\mathcal{M}_{1}$ if and only if $\mu$ is a probability measure on $(X,\mathcal{F})$; and $\mathcal{M}_{1}$ is a set and a subset of $[0,\infty]^{\mathcal{F}}$.