almost all reals are nonzero?

Stream: Is there code for X?

[Alex Kontorovich]

Do we have something like this: almost all reals are not zero?

import Mathlib

example : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume, x ≠ 0 := by
  sorry

Thanks!

[Geoffrey Irving]

docs#MeasureTheory.NoAtoms is the relevant type class.

[Geoffrey Irving]

And then docs#Set.Countable.ae_not_mem will work.