mass_toFiniteMeasure — Mathlib

English

Let μ be a probability measure on Ω. Its associated finite measure μ.toFiniteMeasure has total mass equal to 1.

Русский

Пусть μ – вероятность на Ω. Соответствующая ей конечная мера μ.toFiniteMeasure имеет общую массу, равную 1.

LaTeX

$$$\\operatorname{mass}(\\mu^{\\mathrm{toFiniteMeasure}}) = 1$$$

Lean4

@[simp]
theorem mass_toFiniteMeasure (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasure.mass = 1 :=
  μ.coeFn_univ

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