toNNReal_measureReal_eq_coeFn — Mathlib

English

The finite-measure evaluation agrees with the original probability measure on sets: (μ.toFiniteMeasure)(s) = μ(s).

Русский

Оценка конечной меры совпадает с исходной вероятностной мерой на множествах: (μ.toFiniteMeasure)(s) = μ(s).

LaTeX

$$ (μ.toFiniteMeasure)(s) = μ(s) $$

Lean4

theorem toNNReal_measureReal_eq_coeFn (ν : ProbabilityMeasure Ω) (s : Set Ω) :
    ((ν : Measure Ω).real s).toNNReal = ν s := by simp

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