Theorems · Inductive type · measure theory

MeasureTheory.SMulInvariantMeasure

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

A measure μ : Measure α is invariant under a multiplicative 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

115 results in Mathlib

Foundations

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

Assumes

SMul