Inner regular measures without atoms

A σ-finite, inner regular measure on a Hausdorff space which vanishes on singletons has no atoms. In particular, this applies to locally finite measures on σ-compact metrizable spaces.

theorem MeasureTheory.NoAtoms'.exists_forall_nhds_measure_pos {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} [μ.InnerRegularCompactLTTop] {s : Set α} (meas_s : MeasurableSet s) (hs : 0 < μ s) (hfin : μ s ≠ ⊤) : ∃ x ∈ s, ∀ U ∈ nhds x, 0 < μ (s ∩ U)

Given a measure μ that is inner regular with respect to compact sets, every measurable set s of finite positive measure contains a point x ∈ s such that s ∩ U has positive measure for all neighborhoods U of x.

theorem MeasureTheory.NoAtoms'.of_innerRegularCompactLTTop {α : Type u_1} [TopologicalSpace α] [T2Space α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : Measure α} [NullSingletonClass μ] [μ.InnerRegularCompactLTTop] [SigmaFinite μ] : NoAtoms' μ

A σ-finite measure on a Hausdorff space which is inner regular with respect to compact sets and vanishes on singletons has no atoms. See https://math.stackexchange.com/questions/3881683/does-mu-x-0-imply-non-atomic-for-radon-measure

Proof sketch: an atom s has finite measure by σ-finiteness and thus by exists_forall_nhds_measure_pos contains some x ∈ s such that s ∩ U has positive (hence full) measure for every neighborhood U of x. Now s \ {x} contains a compact L of positive measure, and separating x from L by disjoint open sets yields two disjoint subsets of s of full measure, a contradiction.