English
A Haar measure image under a continuous multiplicative equivalence is Haar.
Русский
Образ меры Хаара под непрерывной мультипликативной эквивалентностью — мера Хаара.
LaTeX
$$$\text{ContinuousMulEquiv.isHaarMeasureMap}$$$
Lean4
/-- A convenience wrapper for `MeasureTheory.Measure.isHaarMeasure_map`. -/
@[to_additive /-- A convenience wrapper for `MeasureTheory.Measure.isAddHaarMeasure_map`. -/
]
nonrec theorem _root_.MulEquiv.isHaarMeasure_map [BorelSpace G] [ContinuousMul G] {H : Type*} [Group H]
[TopologicalSpace H] [MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (e : G ≃* H) (he : Continuous e)
(hesymm : Continuous e.symm) : IsHaarMeasure (Measure.map e μ) :=
let f : G ≃ₜ H := .mk e he hesymm
isHaarMeasure_map μ e.toMonoidHom he e.surjective f.isClosedEmbedding.tendsto_cocompact
