theorem
Topology.IsOpenEmbedding.isHaarMeasure_comap
{G : Type u_1}
{H : Type u_2}
[Group G]
[TopologicalSpace G]
[MeasurableSpace G]
[MeasurableMul G]
[BorelSpace G]
[Group H]
[TopologicalSpace H]
[MeasurableSpace H]
[MeasurableMul H]
[BorelSpace H]
{φ : G →* H}
(hφ : IsOpenEmbedding ⇑φ)
(μ : MeasureTheory.Measure H)
[μ.IsHaarMeasure]
:
(MeasureTheory.Measure.comap (⇑φ) μ).IsHaarMeasure
theorem
Topology.IsOpenEmbedding.isAddHaarMeasure_comap
{G : Type u_1}
{H : Type u_2}
[AddGroup G]
[TopologicalSpace G]
[MeasurableSpace G]
[MeasurableAdd G]
[BorelSpace G]
[AddGroup H]
[TopologicalSpace H]
[MeasurableSpace H]
[MeasurableAdd H]
[BorelSpace H]
{φ : G →+ H}
(hφ : IsOpenEmbedding ⇑φ)
(μ : MeasureTheory.Measure H)
[μ.IsAddHaarMeasure]
: