Positive function integral

Set

 context $M \in \mathrm{MeasureSpace}(X)$
 postulate $\int_X:\mathcal M^+\to \mathbb R_+$
 $f\uparrow u_n$ $u_n\in \mathcal T^+$
 postulate $\int_X\ f\ \mathrm d\mu:=\mathrm{lim}_{n\to \infty}\int_X\ u_n\ \mathrm d\mu$

Notice that the integral on the right hand side here is that for positive real step functions.

Discussion

Monotone convergence theorem:

If $f_n$ is a growing sequence in $\mathcal M^+$, we have

$\int_X\left(\mathrm{lim}_{n\to\infty}f_n\right)\mathrm d\mu=\mathrm{lim}_{n\to\infty}\int_X f_n\mathrm d\mu$