measureReal_ennreal_smul_apply — Mathlib

English

Let μ be a measure on a space and c be a nonnegative extended real. Then the real-valued measure of the scaled measure c • μ on any set s equals c.toReal times μ.real(s).

Русский

Пусть μ — мера на множестве, а c ∈ ℝ≥0∞. Тогда вещевая мера масштаба c • μ на множество s равна c.toReal · μ.real(s).

LaTeX

$$$ (c \\cdot \\mu).real s = c.toReal \\cdot (\\mu.real s) $$$

Lean4

@[simp]
theorem measureReal_ennreal_smul_apply (c : ℝ≥0∞) : (c • μ).real s = c.toReal * μ.real s := by simp [Measure.real]

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