English
The image of a Haar measure under a continuous surjective homomorphism is Haar.
Русский
Образ меры Хаара под непрерывным сюръективным гомоморфизмом есть мера Хаара.
LaTeX
$$$\text{IsHaarMeasure}(\text{Measure.map } f\, \mu)$$$
Lean4
/-- The image of a Haar measure under a continuous surjective proper group homomorphism is again
a Haar measure. See also `MulEquiv.isHaarMeasure_map` and `ContinuousMulEquiv.isHaarMeasure_map`. -/
@[to_additive /-- The image of an additive Haar measure under a continuous surjective proper additive group
homomorphism is again an additive Haar measure. See also `AddEquiv.isAddHaarMeasure_map`,
`ContinuousAddEquiv.isAddHaarMeasure_map` and `ContinuousLinearEquiv.isAddHaarMeasure_map`. -/
]
theorem isHaarMeasure_map [BorelSpace G] [ContinuousMul G] {H : Type*} [Group H] [TopologicalSpace H]
[MeasurableSpace H] [BorelSpace H] [IsTopologicalGroup H] (f : G →* H) (hf : Continuous f) (h_surj : Surjective f)
(h_prop : Tendsto f (cocompact G) (cocompact H)) : IsHaarMeasure (Measure.map f μ) :=
{ toIsMulLeftInvariant := isMulLeftInvariant_map f.toMulHom hf.measurable h_surj
lt_top_of_isCompact := by
intro K hK
rw [← hK.measure_closure, map_apply hf.measurable isClosed_closure.measurableSet]
set g : CocompactMap G H := ⟨⟨f, hf⟩, h_prop⟩
exact IsCompact.measure_lt_top (g.isCompact_preimage_of_isClosed hK.closure isClosed_closure)
toIsOpenPosMeasure := hf.isOpenPosMeasure_map h_surj }
