∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ((∀ᵐ (a : α) ∂μ, a ∈ s) ↔ μ s = μ Set.univ)