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

theorem MeasureTheory.measure_null_iff_eq_empty_of_measure_singleton_ne_zero {α : Type u_1} {F : Type u_2} [FunLike F (Set α) ENNReal] [OuterMeasureClass F α] {μ : F} {s : Set α} (h : ∀ (a : α), μ {a} ≠ 0) : μ s = 0 ↔ s = ∅