Positive real step function
Set
| context | $\langle X,\Sigma\rangle\in\mathrm{MeasurableSpace}(X)$ |
| postulate | $f\in \mathcal T^+$ |
| context | $f\in \mathcal T$ | context | …Real step function |
| $x\in X$ |
| postulate | $f(x)\ge 0$ |
Discussion
Parents
Subset of
| context | $\langle X,\Sigma\rangle\in\mathrm{MeasurableSpace}(X)$ |
| postulate | $f\in \mathcal T^+$ |
| context | $f\in \mathcal T$ | context | …Real step function |
| $x\in X$ |
| postulate | $f(x)\ge 0$ |
