Theorems · Definition · measure theory

MeasurableEquiv.smul

{G : Type u_1} →
  {α : Type u_3} →
    [inst : MeasurableSpace α] → [inst_1 : Group G] → [inst_2 : MulAction G α] → [MeasurableConstSMul G α] → G → α ≃ᵐ α

If a group G acts on α by measurable maps, then each element c : G defines a measurable automorphism of α.

Defined in

Mathlib.MeasureTheory.Group.MeasurableEquiv

Cited by

7 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

MeasurableSpaceGroupMulActionMeasurableConstSMul