===== Positive function integral =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $M \in \mathrm{MeasureSpace}(X)$ |

| @#55EE55: postulate   | @#55EE55: $\int_X:\mathcal M^+\to \mathbb R_+$ |

| $ f\uparrow u_n$ | $u_n\in \mathcal T^+$ |

| @#55EE55: postulate   | @#55EE55: $\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$ ^
==== Parents ====
=== Context ===
[[Growing sequence]], [[Step function integral]], 
[[Positive measurable numerical function]]