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
Context
