Theorems · Definition · measure theory

MeasureTheory.Measure.haar.index

{G : Type u_1} → [Group G] → Set G → Set G → ℕ

The index or Haar covering number or ratio of K w.r.t. V, denoted (K : V): it is the smallest number of (left) translates of V that is necessary to cover K. It is defined to be 0 if no finite number of translates cover K.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Basic

Cited by

20 results in Mathlib

Foundations

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

Assumes

Group