∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  (K : TopologicalSpace.PositiveCompacts G) {V : Set G},
  (interior V).Nonempty → 0 < MeasureTheory.Measure.haar.index (↑K) V