Absolute continuity on a countable type

On a countable type with measurable singletons, absolute continuity is checked on atoms. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean.

theorem MeasureTheory.Measure.absolutelyContinuous_of_forall_singleton {α : Type u_1} [MeasurableSpace α] [Countable α] {μ ν : Measure α} (h : ∀ (a : α), ν {a} = 0 → μ {a} = 0) : μ.AbsolutelyContinuous ν

theorem MeasureTheory.Measure.absolutelyContinuous_iff_forall_singleton {α : Type u_1} [MeasurableSpace α] [Countable α] {μ ν : Measure α} : μ.AbsolutelyContinuous ν ↔ ∀ (a : α), ν {a} = 0 → μ {a} = 0