Theorems · Definition · measure theory

MeasureTheory.Measure.haar

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

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

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroupMeasurableSpaceBorelSpaceLocallyCompactSpace