Theorems · Theorem · measure theory

MeasureTheory.smulInvariantMeasure_map

∀ {M : Type uM} {α : Type uα} {β : Type uβ} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : SMul M α]
  [inst_3 : SMul M β] [MeasurableConstSMul M β] (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure M α μ]
  (f : α → β),
  (∀ (m : M) (a : α), f (m • a) = m • f a) →
    Measurable f → MeasureTheory.SMulInvariantMeasure M β (MeasureTheory.Measure.map f μ)

Defined in

Mathlib.MeasureTheory.Group.Action

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceSMulSMulMeasurableConstSMulMeasureTheory.SMulInvariantMeasure