Atoms of a probability measure on a finite type #
On a finite type with measurable singletons, the real masses of the atoms of a probability
measure sum to one. [UPSTREAM] candidate for Mathlib/MeasureTheory/Measure/Real.lean.
theorem
MeasureTheory.sum_measureReal_singleton_eq_one
{α : Type u_1}
[MeasurableSpace α]
[Fintype α]
[MeasurableSingletonClass α]
(μ : Measure α)
[IsProbabilityMeasure μ]
:
∑ a : α, μ.real {a} = 1