Theorems · Theorem · measure theory

MeasureTheory.Measure.comap_apply

∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) →
      ∀ (μ : MeasureTheory.Measure β), MeasurableSet s → (MeasureTheory.Measure.comap f μ) s = μ (f '' s)

Defined in

Mathlib.MeasureTheory.Measure.Comap

Cited by

14 results in Mathlib

Foundations

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