Nonnegative Measurable Maps and Their Lebesgue Integral

In the setting of Measure Spaces, Borel Sets and Lebesgue Measure on the Real Line: Standing Notation, let $(X,\mathcal{F})$ be a measurable space, let $\mu$ be a measure on $(X,\mathcal{F})$, and let $\mathcal{B}([0,\infty])$ be the Borel $\sigma$-algebra of $[0,\infty]$.

(i) $\mathcal{M}^{+}(X,\mathcal{F})$ is the set $\mathrm{Meas}(X,\mathcal{F};[0,\infty],\mathcal{B}([0,\infty]))$ of Measurable Map, and the Set of Measurable Maps (ii); by Measurable Map, and the Set of Measurable Maps (ii), its elements are exactly the maps $f:X\to[0,\infty]$ that are measurable as maps into $[0,\infty]$.

Let $\mathcal{S}^{+}=\mathcal{S}^{+}(X,\mathcal{F})$ be the set of nonnegative simple functions of Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iii), and $I_{\mu}$ the simple integral of Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv). For $f\in\mathcal{M}^{+}(X,\mathcal{F})$ let $\Sigma_{f}=\{I_{\mu}(s):s\in\mathcal{S}^{+},\ s(x)\le f(x)\text{ for every }x\in X\}$. The condition defining $\Sigma_{f}$, that there is $s\in\mathcal{S}^{+}$ with $v=I_{\mu}(s)$ and $s(x)\le f(x)$ for every $x\in X$, is predicative, with $s(x)\le f(x)$ and $v=I_{\mu}(s)$ written as memberships of ordered pairs in the graphs of $s$, $f$ and $I_{\mu}$ and in $\le$, as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii); so $\Sigma_{f}$ is a class. Then $\Sigma_{f}\subseteq[0,\infty]$ by Simple Functions, Nonnegative Simple Functions, and the Simple Integral (iv), so $\Sigma_{f}$ is a set by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i), and $\Sigma_{f}\neq\emptyset$: for the indicator function $\mathbf{1}_{\emptyset}$ of the empty set, which belongs to $\mathcal{F}$ by Closure Properties of σ-Algebras, Intersections and Traces of σ-Algebras, and the Generated σ-Algebra (vi), $\mathbf{1}_{\emptyset}\in\mathcal{S}^{+}$ by Properties of Simple Functions and of the Simple Integral (i), and for every $x\in X$, $\mathbf{1}_{\emptyset}(x)=0$ by Indicator Function of a Subset (i), as $x\notin\emptyset$, and $0\le f(x)$ by Order and Suprema in the Extended Real Line (viii), as $f(x)\in[0,\infty]$.

(ii) The integral with respect to $\mu$ is the map

$$\mathcal{M}^{+}(X,\mathcal{F})\to[0,\infty],\qquad f\mapsto\int_{X}f\,d\mu=\sup\Sigma_{f}=\sup\bigl\{I_{\mu}(s):s\in\mathcal{S}^{+},\ s(x)\le f(x)\text{ for every }x\in X\bigr\},$$

the supremum being formed in $[-\infty,\infty]$; for each $f\in\mathcal{M}^{+}(X,\mathcal{F})$ it exists by Order and Suprema in the Extended Real Line (iii) and lies in $[0,\infty]$ by Order and Suprema in the Extended Real Line (ix), and the map exists and is unique by Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima (iii), $\le$ being a partial order on $[-\infty,\infty]$ by Order and Suprema in the Extended Real Line (i). The value $\int_{X}f\,d\mu$ is the integral of $f$ with respect to $\mu$, also written $\int f\,d\mu$.