English
If f is locally integrable with respect to μ, then for every scalar c, the function c • f is locally integrable with respect to μ.
Русский
Если f локально интегрируема по μ, то для любого скаляра c функция c • f локально интегрируема по μ.
LaTeX
$$$\operatorname{LocallyIntegrable}(f, \mu) \Rightarrow \forall c\, \operatorname{LocallyIntegrable}(c\cdot f, \mu)$$$
Lean4
protected theorem smul {f : X → E} {𝕜 : Type*} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 E] [IsBoundedSMul 𝕜 E]
(hf : LocallyIntegrable f μ) (c : 𝕜) : LocallyIntegrable (c • f) μ := fun x ↦ (hf x).smul c