Measures having no atoms

class MeasureTheory.NoAtoms' {α : Type u_1} {m0 : MeasurableSpace α} (μ : Measure α) : Prop

Measure μ has no atoms if for any measurable set s with positive μ-measure, there exists a measurable t ⊆ s such that 0 < μ t < μ s. While this implies μ {x} = 0, the converse is not true.

• exists_subset_lt (s : Set α) : 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s

theorem MeasureTheory.NoAtoms'.exists_nullmeasurable_between_measure_eq {α : Type u_1} {m0 : MeasurableSpace α} {μ : Measure α} [na : NoAtoms' μ] {s t : Set α} (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (h : s ⊆ t) {x : ENNReal} (lb : μ s ≤ x) (ub : x ≤ μ t) : ∃ (u : Set α), NullMeasurableSet u μ ∧ s ⊆ u ∧ u ⊆ t ∧ μ u = x