Positive measurable numerical function

Set

 context $\langle X,\Sigma_X\rangle\in \mathrm{MeasurableSpace}(X)$
 postulate $f\in \mathcal M^+$
 context $f\in \mathrm{Measurable}(X,\overline{\mathbb R})$
 $x\in X$
 postulate $f(x)\ge 0$

Discussion

For the definition of the integral, it's crucial to know that for every $f\in \mathcal M^+$, there is a sequence $u_n$ with elements in the step functions $\mathcal T^+$, with $u_n\uparrow f$.