English
The image of a Haar measure under a continuous map is Haar, under suitable hypotheses.
Русский
Образ меры Хаара под непрерывной картой сохраняет свойство Хаара при подходящих условиях.
LaTeX
$$$\text{IsHaarMeasure}(\text{Measure.map } f\, \mu)$$$
Lean4
/-- The image of a finite Haar measure under a continuous surjective group homomorphism is again
a Haar measure. See also `isHaarMeasure_map`. -/
@[to_additive /-- The image of a finite additive Haar measure under a continuous surjective additive group
homomorphism is again an additive Haar measure. See also `isAddHaarMeasure_map`. -/
]
theorem isHaarMeasure_map_of_isFiniteMeasure [BorelSpace G] [ContinuousMul G] {H : Type*} [Group H] [TopologicalSpace H]
[MeasurableSpace H] [BorelSpace H] [ContinuousMul H] [IsFiniteMeasure μ] (f : G →* H) (hf : Continuous f)
(h_surj : Surjective f) : IsHaarMeasure (Measure.map f μ)
where
toIsMulLeftInvariant := isMulLeftInvariant_map f.toMulHom hf.measurable h_surj
toIsOpenPosMeasure := hf.isOpenPosMeasure_map h_surj
