Theorems · Theorem · measure theory

MeasurableEmbedding.restrict_map

∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
  MeasurableEmbedding f →
    ∀ (μ : MeasureTheory.Measure α) (s : Set β),
      (MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))

Defined in

Mathlib.MeasureTheory.Measure.Restrict

Cited by

7 results in Mathlib

Foundations

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