Theorems · Theorem · measure theory

MeasureTheory.Measure.haar.index_defined

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {K V : Set G},
  IsCompact K → (interior V).Nonempty → ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}

If K is compact and V has nonempty interior, then the index (K : V) is well-defined, there is a finite set t satisfying the desired properties.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroup