Pushforward measure

Let $(𝑋, Σ, 𝜇)$ be a measure space, $(𝑌, T)$ be a measurable space, and $𝑓 : 𝑋 \to 𝑌$ is a measurable function, then the pushforward measure on $𝑌$ is given by #m/def/measure

𝑓 * 𝜇 = 𝜇 \circ (𝑓 - 1 ↾ T)

i.e. $𝑓 * 𝜇 (𝐴) = 𝜇 𝑓 - 1 (𝐴)$ .

#state/tidy | #lang/en | #SemBr