Theorems · Definition · measure theory

MeasureTheory.Measure.addHaar

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

addHaar is some choice of a Haar measure, on a locally compact additive group.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

26 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupMeasurableSpaceBorelSpaceLocallyCompactSpace