Lemma about measures that assign non-zero probability to every singleton.

theorem MeasureTheory.Measure.absolutelyContinuous_of_measure_singleton_ne_zero {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} (h : ∀ (a : α), ν {a} ≠ 0) : μ.AbsolutelyContinuous ν