## Real step function

### Set

 context $\langle X,\Sigma\rangle\in\mathrm{MeasurableSpace}(X)$
 postulate $f\in \mathcal T$
 context $f\in\mathrm{Measurable}(X,\mathbb R)$

Where we consider the Borel algebra over $\mathbb R$

 postulate $\mathrm{im}(f)$ … finite

### Discussion

These functions can be written as

$f=\sum_{j=1}^n\alpha_j\cdot\chi_{E_n}$

with $\alpha_j$'s real numbers and $E_n$'s in the measurable algebra.