Measures without atoms on metric spaces

Criteria for measures on (pseudo)metric spaces to have no atoms, in terms of the measures of balls around a fixed center.

theorem MeasureTheory.NoAtoms'.of_metric {α : Type u_1} [PseudoMetricSpace α] [ProperSpace α] [MeasurableSpace α] [OpensMeasurableSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] (c : α) (hμ : ∀ (r : ℝ), μ (Metric.closedBall c r) = μ (Metric.ball c r)) : NoAtoms' μ

theorem MeasureTheory.NoAtoms'.of_metric_of_borelSpace {α : Type u_1} [MetricSpace α] [ProperSpace α] [MeasurableSpace α] [BorelSpace α] {μ : Measure α} [IsFiniteMeasureOnCompacts μ] (c : α) (hμ : ∀ (r : ℝ), μ (Metric.closedBall c r) = μ (Metric.ball c r)) : NoAtoms' μ

Version of of_metric for metric spaces with the Borel σ-algebra, derived from of_innerRegularCompactLTTop: the assumption implies that all spheres around c, and hence all singletons, are null sets.