∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstSMul G α] [MulAction.IsMinimal G α] {U : Set α},
  IsOpen U → U.Nonempty → μ U ≠ ⊤ → MeasureTheory.IsLocallyFiniteMeasure μ