smul — Mathlib

English

The image of a Haar measure under a continuous surjective proper group homomorphism is again a Haar measure.

Русский

Образ меры Хаара под непрерывным сюръективным правильным гомоморфизмом группы снова является мерой Хаара.

LaTeX

$$$\text{IsHaarMeasure}(\text{Measure.map } f\, \mu)$$$

Lean4

@[to_additive IsAddHaarMeasure.smul]
theorem smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) : IsHaarMeasure (c • μ) :=
  { lt_top_of_isCompact := fun _K hK => ENNReal.mul_lt_top ctop.lt_top hK.measure_lt_top
    toIsOpenPosMeasure := isOpenPosMeasure_smul μ cpos }

Похожие утверждения