Documentation

PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef

theorem MeasureTheory.measure_eq_univ_of_forall_singleton {Ω : Type u_1} [Countable Ω] [MeasurableSpace Ω] {μ : Measure Ω} {s : Set Ω} ( : xs, μ {x} = 0) :
μ s = μ Set.univ