map_smul — Mathlib

English

Mapping respects scalar multiplication: (c • v).map f = c • v.map f.

Русский

Отображение сохраняет скалярное умножение: (c • v).map f = c • v.map f.

LaTeX

$$$ (c \\cdot v).map f = c \\cdot (v.map f) $$$

Lean4

@[simp]
theorem map_smul {v : VectorMeasure α M} {f : α → β} (c : R) : (c • v).map f = c • v.map f :=
  by
  by_cases hf : Measurable f
  · ext i hi
    simp [map_apply _ hf hi]
  · simp only [map, dif_neg hf]
      -- `smul_zero` does not work since we do not require `ContinuousAdd`

    ext i
    simp

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