trim_smul — Mathlib

English

Trim respects scalar multiplication: (c • m).trim = c • (m.trim) under appropriate scalar-tower assumptions.

Русский

Обрезка сохраняет умножение на скаляр: (c • m).trim = c • (m.trim) при соответствующих предположениях о тождественных шкалах.

LaTeX

$$$$ (c \cdot m)^{\mathrm{trim}} = c \cdot (m^{\mathrm{trim}}). $$$$

Lean4

/-- `trim` respects scalar multiplication. -/
theorem trim_smul {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (c : R) (m : OuterMeasure α) :
    (c • m).trim = c • m.trim :=
  ext <| trim_op (smul_apply c m)

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