Theorems · Theorem · measure theory

MeasureTheory.isProbabilityMeasure_comap

∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.IsProbabilityMeasure μ] {f : β → α},
  Function.Injective f →
    (∀ᵐ (a : α) ∂μ, a ∈ Set.range f) →
      (∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)) →
        MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.comap f μ)

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasureTheory.IsProbabilityMeasure