English
If f is measure-preserving and a measurable embedding, then for any g: Y → E and any s ⊆ Y, the integral over μ restricted to f^{-1}(s) of g(f(x)) equals the integral over ν restricted to s of g(y).
Русский
Если f сохраняет меру и является измеримо вложением, то для любого g: Y → E и любого s ⊆ Y, интеграл по μ на предобразе f^{-1}(s) от g(f(x)) равен интегралу по ν на s от g(y).
LaTeX
$$$$ \\int_{x \\in f^{-1}(s)} g(f(x)) \\, d\\mu(x) = \\int_{y \\in s} g(y) \\, d\\nu(y) $$$$
Lean4
theorem _root_.Topology.IsClosedEmbedding.setIntegral_map [TopologicalSpace X] [BorelSpace X] {Y} [MeasurableSpace Y]
[TopologicalSpace Y] [BorelSpace Y] {g : X → Y} {f : Y → E} (s : Set Y) (hg : IsClosedEmbedding g) :
∫ y in s, f y ∂Measure.map g μ = ∫ x in g ⁻¹' s, f (g x) ∂μ :=
hg.measurableEmbedding.setIntegral_map _ _
