∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [CompactIccSpace α] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {a b : α}, μ (Set.Ioc a b) < ⊤