map_smul — Mathlib

English

Push-forward commutes with scalar multiplication: (c • ν).map f = c • (ν.map f) for c ∈ ℝ≥0.

Русский

Пересылка меры сохраняет масштабирование: (c • ν).map f = c • (ν.map f).

LaTeX

$$$ (c \\cdot ν).map f = c \\cdot (ν.map f)$ for c ∈ ℝ≥0$$

Lean4

@[simp]
theorem map_smul {f : Ω → Ω'} (c : ℝ≥0) (ν : FiniteMeasure Ω) : (c • ν).map f = c • (ν.map f) :=
  by
  ext s _
  simp [toMeasure_smul]

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