measureReal_nnreal_smul_apply

Mathlib.MeasureTheory.Measure.Real

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measureReal_nnreal_smul_apply

English

For c ∈ ℝ≥0, the real-valued measure of the scaled measure c • μ on a set s is c * μ.real(s).

Русский

Для c ∈ ℝ≥0 реальная мера масштаба c • μ на множество s равна c · μ.real(s).

LaTeX

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

Lean4

@[simp]
theorem measureReal_nnreal_smul_apply (c : ℝ≥0) : (c • μ).real s = c * μ.real s := by simp [measureReal_def]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru