Theorems · Definition · measure theory

MeasureTheory.Measure.haar.prehaar

{G : Type u_1} → [Group G] → [inst : TopologicalSpace G] → Set G → Set G → TopologicalSpace.Compacts G → ℝ

prehaar K₀ U K is a weighted version of the index, defined as (K : U)/(K₀ : U). In the applications K₀ is compact with non-empty interior, U is open containing 1, and K is any compact set. The argument K is a (bundled) compact set, so that we can consider prehaar K₀ U as an element of haarProduct (below).

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

17 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpace