===== Positive measurable numerical function =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $ \langle X,\Sigma_X\rangle\in \mathrm{MeasurableSpace}(X) $ |

| @#55EE55: postulate   | @#55EE55: $f\in \mathcal M^+$ |

| @#55CCEE: context     | @#55CCEE: $f\in \mathrm{Measurable}(X,\overline{\mathbb R})$ |

| $x\in X$ |

| @#55EE55: postulate   | @#55EE55: $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$.
==== Parents ====
=== Subset of ===
[[Measurable numerical function]]