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

Real step function