English
Let μ be a Haar measure on a locally compact group G, and let e: G → H be a continuous multiplicative equivalence. Then the pushforward of μ under e is a Haar measure on H.
Русский
Пусть μ — распределение Хаара на локально компактной группе G, и пусть e: G → H — непрерывное гомоморфное преобразование с обратным отображением. Тогда образ μ по e, т.е. μ map e^{-1}, является распределением Хаара на H.
LaTeX
$$$(e)_*\\mu \text{ is a Haar measure on } H$$$
Lean4
/-- A convenience wrapper for MeasureTheory.Measure.isHaarMeasure_map.
-/
@[to_additive /-- A convenience wrapper for MeasureTheory.Measure.isAddHaarMeasure_map. -/
]
instance _root_.ContinuousMulEquiv.isHaarMeasure_map [BorelSpace G] [IsTopologicalGroup G] {H : Type*} [Group H]
[TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (e : G ≃ₜ* H) :
(μ.map e).IsHaarMeasure :=
e.toMulEquiv.isHaarMeasure_map μ e.continuous e.symm.continuous
