Theorems · Theorem · measure theory

MonoidHom.measurePreserving

∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] {H : Type u_2} [inst_5 : Group H] [inst_6 : TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H]
  [inst_9 : MeasurableSpace H] [BorelSpace H] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure]
  {ν : MeasureTheory.Measure H} [ν.IsHaarMeasure] {f : G →* H},
  Continuous ⇑f → Function.Surjective ⇑f → μ Set.univ = ν Set.univ → MeasureTheory.MeasurePreserving (⇑f) μ ν

A continuous surjective monoid homomorphism of topological groups with compact codomain is measure preserving, provided that the Haar measures on the domain and on the codomain have the same total mass.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

2 results in Mathlib

Foundations

Depth 279 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceGroupIsTopologicalGroupMeasurableSpaceBorelSpaceGroupTopologicalSpaceIsTopologicalGroupCompactSpaceMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsHaarMeasureMeasureTheory.Measure.IsHaarMeasure