Theorems · Definition · measure theory

MeasureTheory.Measure.haar.clPrehaar

{G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] → Set G → TopologicalSpace.OpenNhdsOf 1 → Set (TopologicalSpace.Compacts G → ℝ)

The closure of the collection of elements of the form prehaar K₀ U, for U open neighbourhoods of 1, contained in V. The closure is taken in the space compacts G → ℝ, with the topology of pointwise convergence. We show that the intersection of all these sets is nonempty, and the Haar measure on compact sets is defined to be an element in the closure of this intersection.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpace