Theorems · Theorem · Lie groups

MeasureTheory.Measure.isHaarMeasure_of_isCompact_nonempty_interior

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant] (K : Set G),
  IsCompact K → (interior K).Nonempty → μ K ≠ 0 → μ K ≠ ⊤ → μ.IsHaarMeasure

If a left-invariant measure gives positive mass to some compact set with nonempty interior, then it is a Haar measure.

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

0 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceGroupTopologicalSpaceIsTopologicalGroupBorelSpaceMeasureTheory.Measure.IsMulLeftInvariant