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.

Parents

Refinement of

Measurable function

Context

Real number