integralSum_smul — Mathlib

English

For any scalar c, integralSum(c f) = c integralSum(f).

Русский

Для любого скаляра c выполнено: сумма интеграла от c f равна c раза сумма интеграла от f.

LaTeX

$$$\mathrm{integralSum}(c \cdot f)\;\mathrm{vol}\;\pi = c \; \mathrm{integralSum}(f)\;\mathrm{vol}\;\pi$$$

Lean4

@[simp]
theorem integralSum_smul (c : ℝ) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
    integralSum (c • f) vol π = c • integralSum f vol π := by
  simp only [integralSum, Finset.smul_sum, Pi.smul_apply, ContinuousLinearMap.map_smul]

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