Volume nonzero of nonempty interior

Stream: Is there code for X?

[Alex Kontorovich]

Do we have (perhaps under some conditions) the fact that a MeasurableSet with Nonempty interior has positive measure?

import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

open MeasureTheory Set

example {α : Type _} [TopologicalSpace α] [MeasureSpace α] [BorelSpace α] (s : Set α)
    (hs : Nonempty (interior s)) (s_meas : MeasurableSet s) : 0 < volume s := by
  sorry -- exact? fails

[Anatole Dedecker]

Well it's true (almost) by definition if you have docs#MeasureTheory.Measure.IsOpenPosMeasure

[Alex Kontorovich]

Perfect, exactly what I was looking for, thanks!