Theorems · Inductive type · measure theory

MeasureTheory.VAddInvariantMeasure

(M : Type u_1) → (α : Type u_2) → [VAdd M α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure μ : Measure α is invariant under an additive action of M on α if for any measurable set s : Set α and c : M, the measure of its preimage under fun x => c +ᵥ x is equal to the measure of s.

Defined in

Mathlib.MeasureTheory.Group.Defs

Cited by

114 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

VAdd