English
Let μ, μ′ be Haar measures on a locally compact group G. For an open set s, μ′(s) = haarScalarFactor μ′ μ · μ(s).
Русский
Пусть μ и μ′ — меры Хаара на локально компактной группе G. Для открытого множества s выполняется μ′(s) = haarScalarFactor μ′ μ · μ(s).
LaTeX
$$$\\forall G \\, [\\text{LocallyCompactSpace } G] \\, (μ' : \\mathrm{Measure}(G)) \\, (μ : \\mathrm{Measure}(G)) \\, [\\text{IsHaarMeasure } μ] \\, [\\text{IsHaarMeasure } μ'] \\, {s : \\Set G} \\Rightarrow IsOpen s \\Rightarrow μ' s = haarScalarFactor μ' μ \\cdot μ s$$
Lean4
/-- **Uniqueness of Haar measures**:
Given two Haar measures, they coincide in the following sense: they give the same value to open
sets, up to the multiplicative constant `haarScalarFactor μ' μ`. -/
@[to_additive measure_isAddHaarMeasure_eq_smul_of_isOpen /-- **Uniqueness of Haar measures**:
Given two additive Haar measures, they coincide in the following sense: they give the same value to
open sets, up to the multiplicative constant `addHaarScalarFactor μ' μ`. -/
]
theorem measure_isHaarMeasure_eq_smul_of_isOpen [LocallyCompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
[IsHaarMeasure μ'] {s : Set G} (hs : IsOpen s) : μ' s = haarScalarFactor μ' μ • μ s :=
measure_isHaarMeasure_eq_smul_of_isEverywherePos μ' μ hs.measurableSet hs.isEverywherePos
