===== Real step function =====
==== Set ====
| @#55CCEE: context     | @#55CCEE: $\langle X,\Sigma\rangle\in\mathrm{MeasurableSpace}(X)$ |

| @#55EE55: postulate   | @#55EE55: $f\in \mathcal T$ |

| @#55CCEE: context     | @#55CCEE: $f\in\mathrm{Measurable}(X,\mathbb R)$ |

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

| @#55EE55: postulate   | @#55EE55: $\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]]