English
Let μ, μ′ be left-invariant Haar-type measures on G. If μ and μ′ are inner regular, then μ′ = haarScalarFactor μ′ μ · μ.
Русский
Пусть μ и μ′ — лево-инвариантные меры на G, обе внутренне регулярны; тогда μ′ = haarScalarFactor μ′ μ · μ.
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsFiniteMeasureOnCompacts } μ'] \\, [\\text{IsMulLeftInvariant } μ'] \\, [\\text{InnerRegular } μ] \\, [\\text{InnerRegular } μ'] \\, μ' = haarScalarFactor μ' μ · μ$$
Lean4
/-- **Uniqueness of left-invariant measures**:
Two Haar measures coincide up to a multiplicative constant in a second countable group. -/
@[to_additive isAddLeftInvariant_eq_smul]
theorem isMulLeftInvariant_eq_smul [LocallyCompactSpace G] [SecondCountableTopology G] (μ' μ : Measure G)
[IsHaarMeasure μ] [IsFiniteMeasureOnCompacts μ'] [IsMulLeftInvariant μ'] : μ' = haarScalarFactor μ' μ • μ :=
isMulLeftInvariant_eq_smul_of_regular μ' μ
