isMulInvariant_eq_smul_of_compactSpace

English

Two left-invariant measures with finite values on compacts agree on closures of sets up to haar scalar factor.

Русский

Две левые инвариантные меры с конечной массой на компактном множестве соглашаются на замыканиях множеств до коэффициента Хаара.

LaTeX

$$$$ μ'(closure(s)) = haarScalarFactor μ' μ · μ(closure(s)). $$$$

Lean4

/-- **Uniqueness of Haar measures**:
Two Haar measures on a compact group coincide up to a multiplicative factor. -/
@[to_additive isAddInvariant_eq_smul_of_compactSpace]
theorem isMulInvariant_eq_smul_of_compactSpace [CompactSpace G] (μ' μ : Measure G) [IsHaarMeasure μ]
    [IsMulLeftInvariant μ'] [IsFiniteMeasureOnCompacts μ'] : μ' = haarScalarFactor μ' μ • μ :=
  by
  ext s _hs
  exact measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact

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