sum_smul_dirac — Mathlib

English

A measure on a countable space is the sum of Dirac measures weighted by the masses at each point.

Русский

Мера на счётном пространстве есть сумма мер Дирака, взвешенная массами в каждой точке.

LaTeX

$$$ μ = \\sum a : α \\; μ({a}) · dirac a $$$

Lean4

/-- A measure on a countable type is a sum of Dirac measures. -/
@[simp]
theorem sum_smul_dirac [Countable α] [MeasurableSingletonClass α] (μ : Measure α) :
    (sum fun a => μ { a } • dirac a) = μ := by simpa using (map_eq_sum μ id measurable_id).symm

Похожие утверждения