smul_toOuterMeasure — Mathlib

English

Scaling a measure scales its outer measure correspondingly: (c • μ).toOuterMeasure = c • μ.toOuterMeasure.

Русский

Умножение меры на скаляр пропорционально масштабирует её внешнюю меру: (c • μ).toOuterMeasure = c • μ.toOuterMeasure.

LaTeX

$$$ (c \cdot \mu).toOuterMeasure = c \cdot \mu.toOuterMeasure. $$$

Lean4

@[simp]
theorem smul_toOuterMeasure {_m : MeasurableSpace α} (c : R) (μ : Measure α) :
    (c • μ).toOuterMeasure = c • μ.toOuterMeasure :=
  rfl

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