Measurable function

Set

 context $\langle X,\Sigma_X\rangle\in \mathrm{MeasurableSpace}(X)$ context $\langle Y,\Sigma_Y\rangle\in \mathrm{MeasurableSpace}(Y)$
 postulate $f\in \mathrm{Measurable}(X,Y)$
 context $f:X\to Y$ $y\in \Sigma_Y$
 postulate $f^{-1}(y)\in\Sigma_X$

Discussion

This is very similar to the definition of continuous function.

People write $f:\langle X,\Sigma_X\rangle\to\langle Y,\Sigma_Y\rangle$ to point out the function is measurable, although I'd say that's abuse of language.

Reference

Wikipedia: Sigma-algebra