Theorems · Definition · measure theory

MeasureTheory.FiniteMeasure.map

{Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] → MeasureTheory.FiniteMeasure Ω → (Ω → Ω') → MeasureTheory.FiniteMeasure Ω'

The push-forward of a finite measure by a function between measurable spaces.

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

16 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace