toSignedMeasure_smul — Mathlib

English

For NNReal r, (r • μ).toSignedMeasure = r • μ.toSignedMeasure.

Русский

Для NNReal r выполняется (r • μ).toSignedMeasure = r • μ.toSignedMeasure.

LaTeX

$$$ (r \cdot μ).toSignedMeasure = r \cdot μ.toSignedMeasure $$$

Lean4

@[simp]
theorem toSignedMeasure_smul (μ : Measure α) [IsFiniteMeasure μ] (r : ℝ≥0) :
    (r • μ).toSignedMeasure = r • μ.toSignedMeasure := by
  ext i hi
  rw [toSignedMeasure_apply_measurable hi, VectorMeasure.smul_apply, toSignedMeasure_apply_measurable hi,
    measureReal_nnreal_smul_apply]
  rfl

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