Step function integral

Set

context $\langle X,\Sigma,\mu\rangle\in \mathrm{MeasureSpace}(X)$
postulate $\int_X:\mathcal T^+\to \mathbb R_+$
$ f\equiv \sum_{j=1}^n\alpha_j\cdot\chi_{E_n} \in \mathcal T^+$
postulate $\int_X\ f\ \mathrm d\mu:=\sum_{j=1}^n\alpha_j\cdot\mu(E_n) $

Discussion

Reference

Parents

Context

Positive real step function, Characteristic function, Finite sum of complex numbers