Theorems · Definition · measure theory

MeasurableEquiv.vadd

{G : Type u_1} →
  {α : Type u_3} →
    [inst : MeasurableSpace α] →
      [inst_1 : AddGroup G] → [inst_2 : AddAction G α] → [MeasurableConstVAdd G α] → G → α ≃ᵐ α

If an additive 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

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceAddGroupAddActionMeasurableConstVAdd