Positive function integral

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.

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$