Theorems · Theorem · measure theory

MeasureTheory.Measure.NullMeasurableSet.image

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

Defined in

Mathlib.MeasureTheory.Measure.Comap

Cited by

1 results in Mathlib

Foundations

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