Theorems · Definition · measure theory

MeasureTheory.Measure.addHaarMeasure

{G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalAddGroup G] →
        [inst : MeasurableSpace G] → [BorelSpace G] → TopologicalSpace.PositiveCompacts G → MeasureTheory.Measure G

The Haar measure on the locally compact additive group G, scaled so that addHaarMeasure K₀ K₀ = 1.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

21 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupMeasurableSpaceBorelSpace