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

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

| @#55CCEE: context     | @#55CCEE: $f\in \mathcal T$ | @#55CCEE: context     | @#55CCEE: ...[[Real step function]] | 

| $x\in X$ |

| @#55EE55: postulate   | @#55EE55: $f(x)\ge 0$ |

==== Discussion ====
==== Parents ====
=== Subset of ===
[[Real step function]]