English
The image of a finite Haar measure under a continuous surjective group homomorphism is again a Haar measure.
Русский
Образ конечной меры Хаара под непрерывным сюръективным гомоморфизмом группы снова является мерой Хаара.
LaTeX
$$$\text{IsHaarMeasure}(\text{Measure.map } f\, \mu)$$$
Lean4
/-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
it is a Haar measure. -/
@[to_additive /-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then
it is an additive Haar measure. -/
]
theorem isHaarMeasure_of_isCompact_nonempty_interior [IsTopologicalGroup G] [BorelSpace G] (μ : Measure G)
[IsMulLeftInvariant μ] (K : Set G) (hK : IsCompact K) (h'K : (interior K).Nonempty) (h : μ K ≠ 0) (h' : μ K ≠ ∞) :
IsHaarMeasure μ :=
{ lt_top_of_isCompact := fun _L hL => measure_lt_top_of_isCompact_of_isMulLeftInvariant' h'K h' hL
toIsOpenPosMeasure := isOpenPosMeasure_of_mulLeftInvariant_of_compact K hK h }
