Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.map_smul

∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {f : Ω → Ω'} (c : NNReal)
  (ν : MeasureTheory.FiniteMeasure Ω), (c • ν).map f = c • ν.map f

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpace