Theorems · Theorem · measure theory

Topology.IsClosedEmbedding.setIntegral_map

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} [inst_2 : TopologicalSpace X] [BorelSpace X] {Y : Type u_5} [inst_4 : MeasurableSpace Y]
  [inst_5 : TopologicalSpace Y] [BorelSpace Y] {g : X → Y} {f : Y → E} (s : Set Y),
  Topology.IsClosedEmbedding g → ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map g μ = ∫ (x : X) in g ⁻¹' s, f (g x) ∂μ

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

0 results in Mathlib

Foundations

Depth 257 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceTopologicalSpaceBorelSpaceMeasurableSpaceTopologicalSpaceBorelSpace