smul — Mathlib

English

If HasIntegral I l f vol y holds, then for any real scalar c, HasIntegral I l (c • f) vol (c • y).

Русский

Если HasIntegral для f существует с y, то для любого коэффициента c выполняется HasIntegral для c•f с c•y.

LaTeX

$$$\forall (hf : HasIntegral I l f vol y) (c : \mathbb{R}), HasIntegral I l (c \cdot f) vol (c \cdot y)$$$

Lean4

theorem smul (hf : HasIntegral I l f vol y) (c : ℝ) : HasIntegral I l (c • f) vol (c • y) := by
  simpa only [HasIntegral, ← integralSum_smul] using (tendsto_const_nhds : Tendsto _ _ (𝓝 c)).smul hf

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