Theorems · Theorem · measure theory

MeasureTheory.vaddInvariantMeasure_map

∀ {M : Type uM} {α : Type uα} {β : Type uβ} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : VAdd M α]
  [inst_3 : VAdd M β] [MeasurableConstVAdd M β] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ]
  (f : α → β),
  (∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a) →
    Measurable f → MeasureTheory.VAddInvariantMeasure 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

MeasurableSpaceMeasurableSpaceVAddVAddMeasurableConstVAddMeasureTheory.VAddInvariantMeasure