Theorems · Theorem · Lie groups

MeasureTheory.measure_univ_of_isMulLeftInvariant

∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] [inst_3 : Group G]
  [IsTopologicalGroup G] [WeaklyLocallyCompactSpace G] [NoncompactSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsOpenPosMeasure] [μ.IsMulLeftInvariant], μ Set.univ = ⊤

In a noncompact locally compact group, a left-invariant measure which is positive on open sets has infinite mass.

Defined in

Mathlib.MeasureTheory.Group.Measure

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceBorelSpaceGroupIsTopologicalGroupWeaklyLocallyCompactSpaceNoncompactSpaceMeasureTheory.Measure.IsOpenPosMeasureMeasureTheory.Measure.IsMulLeftInvariant