Theorems · Definition · measure theory

MeasureTheory.Measure.map

{α : Type u_4} →
  {β : Type u_5} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → (α → β) → MeasureTheory.Measure α → MeasureTheory.Measure β

The pushforward of a measure. It is defined to be 0 if f is not an almost everywhere measurable function.

Defined in

Mathlib.MeasureTheory.Measure.Map

Cited by

858 results in Mathlib

Foundations

Depth 195 from the axioms, rests on 4,758 definitions · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceMeasurableSpace