theorem
MeasureTheory.NoAtoms'.of_metric
{α : Type u_1}
[ne : Nonempty α]
[PseudoMetricSpace α]
[ProperSpace α]
[MeasurableSpace α]
[OpensMeasurableSpace α]
{μ : Measure α}
[IsFiniteMeasureOnCompacts μ]
(hμ : ∀ (r : ℝ), μ (Metric.closedBall ne.some r) = μ (Metric.ball ne.some r))
:
NoAtoms' μ
instance
MeasureTheory.NoAtoms'.instOfBorelSpaceOfFiniteDimensionalRealOfIsAddHaarMeasureOfNontrivial
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[FiniteDimensional ℝ E]
(μ : Measure E)
[μ.IsAddHaarMeasure]
[Nontrivial E]
:
NoAtoms' μ