Theorems · Definition · measure theory

MeasurableEquiv.mulLeft

{G : Type u_1} → [inst : Group G] → [inst_1 : MeasurableSpace G] → [MeasurableMul G] → G → G ≃ᵐ G

If G is a group with measurable multiplication, then left multiplication by g : G is a measurable automorphism of G.

Defined in

Mathlib.MeasureTheory.Group.MeasurableEquiv

Cited by

9 results in Mathlib

Foundations

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

Assumes

GroupMeasurableSpaceMeasurableMul